Type checking and normalisation

James Chapman

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