*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.

- Inductive definitions and pattern matching in Type Theory
- Internal Type Theory
- Domain specific extensions and their framework
- Ordinals in Type Theory
- Formal Topology
- Computational content of classical logic

For papers on this topic, see the home pages of

Last modified: Wed May 27 13:43:48 MET DST 1998