## Type checking and normalisation

School of Computer Science

University of Nottingham

Tuesday, 18 November 2008, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: Implementations of Martin-Löf's type theory
can be used to support the development of dependently typed programs
and machine checked mathematics. At the heart of any such
implementation is a type checker, and at the heart of any such type
checker is a normaliser. In this talk I will introduce type theory,
describe why one might want to write a type checker for type theory in
type theory, and then describe how to write a normaliser for
λ^{σ}-calculus as a dependently typed
program.

Tarmo Uustalu

Last update 19.11.2008