[TAPL] Lecture 3. Lambda calculus

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