Formalization of the book "Type Theory and Formal Proof: An Introduction" in Agda.
- Untyped Lambda Calculus
-
Simply Typed Lambda Calculus (
$\lambda ^ \to$ ) -
Second-order Typed Lambda Calculus (
$\lambda 2$ )
Caution
Be sure to review the book's errata (page 51).
BSD-3-Clause