This is a formal verification of de Groote's λλ type system, as specified in his paper "Defining λ-Typed λ-Calculi by Axiomatizing the Typing Relation".
Some highlights of the project:
- De Bruijn indices are used
- "Types" are lambda expressions
- There are no Pi types, only Lambda expressions and Lambda kinds