A series of Lambda Calculus implementations starting from Simply Typed evaluation, then work up through bidirectional typechecking, normalization by evaluation, elaboration and then various type system extensions.
The goal is to provide best practices examples of all the features you might want to include in your custom language in one place.
- SimplyTypedEvaluation
- BidirectionalTypechecking
- NormalizationByEvaluation
- Elaboration
- TypedHoles
- SystemT
- Records
- Subtyping
- Nominal Inductive Types
- Iso-Inductive Types
- System F
- Martin-Lof Type Theory (Pi and Sigma Types)
- Universes
- Indexed Inductive Types
- Equality
- Case-Trees
- Row Polymorphism
- Linear Types
