Type Theory and Formal Proof: An Introduction

This is a formalization of the book "Type Theory and Formal Proof: An Introduction" by Rob Nederpelt and Herman Geuvers.

Chapters

1. Untyped Lambda Calculus
2. Simply Typed Lambda Calculus (${\lambda }^{\to }$)
3. Second-order Typed Lambda Calculus ($\lambda 2$)
4. Types Dependent on Types ($\lambda \underset{―}{\omega }$)

Caution

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

License

BSD-3-Clause