Simply-Typed Lambda Calculus
This is the simply-typed lambda calculus with integers and
addition. Of particular
interest in this example is the proof of progress, particularly
the way canonical form lemmas are proven.
- Host language: Simply-typed
lambda calculus with integers and addition proving uniqueness of
evaluation, type preservation, and progress
- Let extension: New syntax for let
expressions
- Pair extension: New syntax for
pair expressions
