Lambda calculus and types

Lecturer

Thorsten Altenkirch, University of Nottingham

Abstract

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