Lambda Calculus and Types

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

Outline

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

TBA