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
- Untyped Lambda Calculus
- Simply Typed Lambda Calculus (
) - Second-order Typed Lambda Calculus (
) - Types Dependent on Types (
)
[!CAUTION] Be sure to review the book's errata (page 51).
License
BSD-3-Clause