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.