Grimoire of Alice includes all things PL and TT.
- Terms.agda Simply-typed lambda calculus with intrinsically-scoped intrinsically-typed terms and deBrujin indices.
- Reduction.agda Reduction rules for simply-typed lambda calculus.
- CatSem.agda Formalization of the categorical semantics of STLC.
- Typecheck.agda Certified type checker.
- Inference.agda Certified bidirectional type inference.
- Untyped.agda Untyped lambda calculus and its reduction rules.
- haskell/ Haskell implementation of STLC.