keilambda/ttfpi-agda

Formalization of the book "Type Theory and Formal Proof: An Introduction" in Agda

Type Theory and Formal Proof: An Introduction

Formalization of the book "Type Theory and Formal Proof: An Introduction" in Agda.

Chapters

1. Untyped Lambda Calculus
2. Simply Typed Lambda Calculus ($\lambda ^ \to$)
3. Second-order Typed Lambda Calculus ($\lambda 2$)

Caution

Be sure to review the book's errata (page 51).

License

BSD-3-Clause