Lambda calculus and types


Thorsten Altenkirch, University of Nottingham


The lambda calculus as an abstract theory of function is an important tool in theoretical computer science. In this introductory course we introduce the basic, untyped lambda calculus, basic notions like alpha, beta and eta equivalence, combinatory logic and simple types and their semantics. We will demonstrate the use of semantic notions to construct normalisation proofs by introducing normalisation by evaluation.

Thorsten Altenkirch
Last modified: Wed Feb 4 17:25:34 GMT 2004