Semantics refers here on the one hand to the inuitive informal meaning explanations developed by Martin-Löf in the tradition of intuitionistic philosophy of mathematics, and on the other hand to metamathematical modelling. Such modelling has provided mathematically rigorous proofs of consistency, decidability of the formal judgements, and other key properties of the system.
Proof theory refers to the part of logic in which proofs are considered as mathematical objects and as such become the subject of metamathematical study. The development of Type Theory was influenced by the proof-theoretic tradition and early papers often discuss typical proof-theoretic issues such as proof normalization and proof-theoretic strength (ordinal analysis).
We will here investigate several topics in semantics and proof theory with the aim to increase our understanding of Type Theory. Our interest in these topics comes in many cases from questions encountered during use and implementation of Type Theory. We have ample evidence that metatheoretical investigations can influence issues of more immediate practical relevance, sometimes in an unexpected way.
For papers on this topic, see the home pages of