Skip to content

sequents/code

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Sequents

Code for proof theory webinar series

Past videos: https://www.youtube.com/channel/UC8reF8xuw05LOYLeWNRV0pg

TG chat group: @proof_theory

Sessions

  1. Untyped lambda calculus: named
  2. Untyped lambda calculus: DeBrujin indices, strong reduction, abstract machines, scoped terms
  3. Simply typed lambda calculus: Nat/Fin/Elem, smallstep reduction, KAM(0) & C(E)K machines
  4. STLC parser & bidirectional typechecker, PCF terms, smallstep & machines
  5. PCF untyped & typed bytecode, simple compiler and virtual machine
  6. PCF compiler & virtual machine, basics of lambda-mu calculus
  7. Lambda-mu calculus: Parigot, Saurin and Ariola's variations
  8. LJ, LJT & LJTPCF calculi
  9. Three bidirectional tricks: semiannotated lambdas, detalized errors and LJT checker derivation
  10. Big-step reduction, LJQ and 2 variants of LJQPCF