Lambda Calculus

This is the lambda calculus with typing added in an extension.

Note the projection constraints proj_subst_same and proj_eval_same given by the host language. These require substitution and evaluation to give the same results across projections. These constraints make it possible for an extension to add typing and prove type preservation, but it means new constructs can be little more than syntactic sugar when it comes to evaluation.

• Host language: Untyped lambda calculus with evaluation
• Typing extension: Adds typing for the language and proves type preservation
• Let extension: Adds let expressions to the language
• Pair extension: Adds pairs with selectors for the elements to the language
• Boolean extension: Adds Boolean true and false, along with conditionals, to the language

Download example tarball

Back to examples