Walkthrough

This is a simple language as a starting point for new users, the language used in the walkthrough, based on the language in "Sound type-dependent syntactic language extension".

• Host language: Simply-typed lambda calculus proving type preservation
• Let extension: New syntax for let expressions
• Big step evaluation extension: New relation for big-step evaluation and type preservation for it

Download example tarball

Back to examples