Home

• 2019.01.05 - Session 1: Untyped named lambda calculus
• 2019.01.14 - Session 2: DeBruijn indices, strong reduction, abstract machines & scoped LC
• 2019.01.21 - Session 3: Simply typed lambda calculus: Nat/Fin/Elem, smallstep reduction, KAM(0) & C(E)K machines
• 2019.02.06 - Session 4: STLC parser & bidirectional typechecker, PCF terms, smallstep & machines
• 2019.02.18 - Session 5: PCF untyped & typed bytecode, simple compiler and virtual machine
• 2019.06.05 - Session 6: PCF compiler & virtual machine, basics of lambda-mu calculus
• 2019.09.28 - Session M: Modal types for fun & profit (Scala Russia 2019)
• 2019.11.20 - Session 7: Lambda-mu calculus: Parigot, Saurin and Ariola's variations
• 2020.04.11 - Session 8: LJ, LJT & LJTPCF calculi
• 2020.09.05 - Session 9: Three bidirectional tricks: semiannotated lambdas, detalized errors and LJT checker derivation
• 2021.01.04 - Session 10: Big-step reduction, LJQ and 2 variants of LJQPCF