Ch.5 The Untyped Lambda Calculus

• Lambda calculus
  • Peter Landin observed that a complex programming language can be understood by formulating it as a tiny core calculus capturing the language's essential mechanisms, together with a collection of convenient derived forms whose behavior is understood by translating them into the core.
  • The core language used by Landin,  was the Lambda calculus, invented by Alonzo church.
  • Cf. Core calculi
    • Alonzo Church : Lambda calculus
    • Robin Milner et al : Pi calculus
    • Abadi and Cardelli : Object calculus
• The Syntax and semantics of lambda calculus

• Church encoding
  • true, false, and, or, not
  • pair, fst, snd,
  • church numerals, add, times, ...
• The enriched lambda calculus
  • boolean and arithmetic expression
  • recursion
• Formalities
  • FV
  • substitution

Ch.9 Simple Typed Lambda Calculus