Lambda Calculus and Types

Practical introduction to lambda calculus (thus excluding, e.g., computability theory). May be interleaved with FP.


  • Untyped lambda calculus (1 unit)
    • Syntax, alpha-conversion, beta-reduction
    • Reduction strategies & Church-Rosser Theorem
    • Programming in lambda calculus
      • Church numerals
      • Fixed-point combinator
  • Simply typed lambda calculus (1 unit)
    • Typing rules (à la Curry)
    • Simply typed lambda calculus à la Church
    • Type safety
      • Subject reduction, progress, and strong normalisation
    • Programming with simply typed lambda calculus
      • Folds
  • Polymorphic lambda calculus (1 unit)
    • Typing rules
    • Church numerals and folds revisited
    • Special case: Hindley-Milner & Algorithm W

Course Materials