Session 3

Simply typed lambda calculus: Nat/Fin/Elem, smallstep reduction, KAM(0) & C(E)K machines

• DeBruijn chapter of PLFA (& surrounding chapters)
• STLC chapter of SF (& surrounding chapters)
• Swierstra, "From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine"
  • Idris port
• SECD machine:
  • Landin, "The mechanical evaluation of expressions"
  • Danvy, "A Rational Deconstruction of Landin's SECD Machine"
• Machines for strong reduction:
  • Cregut, "Strongly Reducing Variants of the Krivine Abstract Machine"
  • Kluge, "Abstract Computing Machines" (sec 6.4)
  • https://github.com/clayrat/sequent-calc/tree/master/src/Lambda/Untyped/Strong
  • Gregoire, Leroy, "A Compiled Implementation of Strong Reduction"

Homework

• Напишите call-by-value и сильную (CBN или CBV) small-step редукции для Lambda.STLC
• Посмотрите на реализацию SECD-машины в Lambda.STLC.SECD. Можно ли переписать её проще в стиле KAM/CEK?