One particular goal is to develop Internal Type Theory, that is, the internalization of the syntax and semantics (and more generally the metatheory) of Type Theory using itself as metalanguage. Here it is important to view Type Theory as an open, extensible theory; we can of course not prove consistency of a fixed theory in itself. We wish in particular to formalize (i) the syntax of Type Theory including a general system of inductive and inductive-recursive definitions; (ii) the intended semantics of Type Theory, perhaps using a variant of Martin-Löf's Tarski semantics of Type Theory or Hofmann's setoid model of Type Theory; (iii) prove decidability of the judgements of Type Theory as a consequence of a reduction-free normalization proof.
For the syntax we have taken a categorical approach and introduced the notion of category with families (cwf). This improves upon Cartmell's categories with attributes, yielding a variable-free syntax closely related to Martin-Löf's explicit substitution calculus. Furthermor, we have begun formalizing constructive Category Theory inside Type Theory in order to obtain a definition of internal cwfs as the basis of Internal Type Theory. We have also provided a finite axiomatization of inductive-recursive definitions which could be useful for internalization. We have begun the construction of internal models. Dybjer defined a cwf of normal term and conjectured that this could be used to prove a coherence result for Type Theory. Gaspes extended Martin-Löf's approach to Tarski semantics of Type Theory (also based on cwfs) to non-standard Type Theory. Relevant are also our studies of reduction-free normalization of simpler systems. It remains to carry out the program of internalizing the proof of normalization, and further to extend the eta-expansion approach to the full system of inductive types. The latter would need some important new idea. Finally, coherence problems seem crucial for Internal Type Theory. We have studied several such from a type-theoretic viewpoint.
Our studies of have highlighted problems relating to equality in Intensional Type Theory - the theory which underlies present proof editors. It seems that many proofs in constructive model theory would become significantly simpler in Extensional Type Theory. Since it is easier to implement efficient proof assistants for Intensional Type Theory it becomes important to understand how to reason with extensional concepts in Intensional Type Theory or in an extension of it. One relevant construction here is the setoid model of Hofmann~. We would like to extend this model and also develop it formally inside Intensional Type Theory.
We would also like to make further investigations of Martin-Löf's meaning explanations and their relationship to game semantics with the hope that this will throw further light on the question of equality in Type Theory.