Session 1

Untyped named lambda calculus

• https://en.wikipedia.org/wiki/Proof_theory
• https://github.com/mietek/cook
• Benjamin C. Pierce, "Types and Programming Languages"
• W. Kluge, "Abstract Computing Machines"
• J.R. Hindley, J.P. Seldin, "Lambda Calculus and Combinators" (2008)

Misc links

• http://www.madore.org/~david/programs/unlambda/ язык на SKI-комбинаторах (соответствует системе Гильберта)

Homework

• Попробуйте спортировать определения термов (Lambda.Untyped.TermNam) и пошагового интерпретатора (Lambda.Untyped.SmallstepNam) на ваш любимый язык.
• В качестве спойлера посмотрите самостоятельно остальные файлы в Lambda.Untyped:
  • Lambda.Untyped.{TermDB, SmallstepDB} - безымянное представление ДеБрёйна
  • Lambda.Untyped.{KAM, CEK} - абстрактные машины