Typed Lambda-Calculus

Paul Levy (Birmingham)

This course is an introduction to the typed lambda-calculus, a language for describing functions and tuples, with sum, product and function types. We look at denotational semantics, using sets and functions, the substitution lemma and equational theory. We then explore some consequences of adding computational effects, under call- by-value and call-by-name evaluation.

Part 1: Concepts and Syntax
Part 2: Substitution and Equations
Part 3: From Pure to Effectful
Part 4: Denotational Semantics of Call-By-Value
Answers to Part 1's exercises, and further questions

Last modified: Fri Jan 10 16:12:41 GMT 2014