# 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