Abstracts.2021.Norm.DTT

Canonicity and normalisation for dependent type theory

by Thierry Coquand

Abstract

The first part will consist of some historical remarks about the problem of normalisation for type systems, mentioning Hilbert, Gödel, Tait, Girard, Martin-Löf and Hancock.

I will then go through the various proofs from Martin-Löf (between 1971 and 1979), and what were the remaining problems, and then present a general technique for handling these problems. If time allows, I also will show how this technique applies when one adds modal operations.

References

TBD