ry far based on the Curry-Horward correspondance, and essentially all of logic and (arguably) mathematics can be built using a similar process.</p>
<p>At least it is hoped that the previous examples provide a good illustration of the deep connection existing between computation (types, expressions, function application) and reasoning (propositions, proofs, deduction) in a typed lambda-calculus.</p>
<p>It is now time to be a little bit more explicit about the particular calculus implemented in LaTTe.</p>
<h2