Code for proof theory webinar series
Past videos: https://www.youtube.com/channel/UC8reF8xuw05LOYLeWNRV0pg
TG chat group: @proof_theory
- Untyped lambda calculus: named
- Untyped lambda calculus: DeBrujin indices, strong reduction, abstract machines, scoped terms
- Simply typed lambda calculus: Nat/Fin/Elem, smallstep reduction, KAM(0) & C(E)K machines
- STLC parser & bidirectional typechecker, PCF terms, smallstep & machines
- PCF untyped & typed bytecode, simple compiler and virtual machine
- PCF compiler & virtual machine, basics of lambda-mu calculus
- Lambda-mu calculus: Parigot, Saurin and Ariola's variations
- LJ, LJT & LJTPCF calculi
- Three bidirectional tricks: semiannotated lambdas, detalized errors and LJT checker derivation
- Big-step reduction, LJQ and 2 variants of LJQPCF