Skip to content

Abstracts.2021.Norm.DTT

Jump to bottom
Fabian edited this page Feb 4, 2022 · 5 revisions

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.

Lecture material

Bibliography

  1. Per Martin-Löf. A theory of types. Preprint, Stockholm University, 1971.
  2. Per Martin-Löf. Hauptsatz for the intuitionistic theory of iterated inductive definitions. Second Scandinavian Logic Symposium (Oslo, 1970), pp. 179–216. Studies in Logic and the Foundations of Mathematics 63, 1971.
  3. Per Martin-Löf. An intuitionistic theory of types. Twenty Five Years of Constructive Type Theory (Venice, 1995), pp. 127–172. Oxford Logic Guides 36, 1998.
  4. Per Martin-Löf. An intuitionistic theory of types: predicative part. Logic Colloquium 1973 (Bristol, 1973), pp. 73–118. Studies in Logic and the Foundations of Mathematics 80, 1975.
  5. Per Martin-Löf. About models for intuitionistic type theories and the notion of definitional equality. Third Scandinavian Logic Symposium (Uppsala, 1973), pp. 81–109. Studies in Logic and the Foundations of Mathematics 82, 1975.
  6. Per Martin-Löf. Constructive mathematics and computer programming. Logic, Methodology and Philosophy of Science VI (Hannover, 1979), pp. 153–175. Studies in Logic and the Foundations of Mathematics 104, 1982.
  7. Thierry Coquand. Canonicity and normalisation for Dependent Type Theory. arXiv:1810.09367v1 [cs.PL], 2018.
Clone this wiki locally