Extensions of Type Theory by inductive definitions were originally justified by Martin-Löf's informal meaning explanations. However, the inherent informality of Martin-Löf's explanation made it somewhat unclear when an addition needed for applications should be accepted. It therefore became an important task to make the underlying principles precise.
Several methods were proposed. For example, Dybjer showed how to use encodings in terms of wellordering sets. Coquand and Paulin proposed a categorical method using initial algebra semantics. Works by Martin-Löf and Backhouse on schematic presentations was generalized to dependent types by Coquand and Paulin and by Dybjer Inductive definitions obtained by specializing these schemata were heavily used in formal proofs developed in the ALF family of proof editors (see the project ``Editors for proofs and programs'').
Another important extension which facilitated the writing of programs and proofs in ALF is Coquand's pattern matching on dependent types. This allowed a more flexible and user-friendly style of recursive function definitions than the original encoding via elimination constans.
The role of models. While designing the schemata for inductive definitions, the simultaneous development of mathematical models was essential. A feature of the model often suggested a possible generalization or a necessary restriction of proposed formal systems.
Plans. A model constructed by Hofmann and Streicher showed that ALF's pattern matching is a non-conservative extension. This led Coquand to restrict the schema for inductive definitions so that it interacted more harmoniously with pattern matching in the HALF-system, a recently implemented successor of ALF. However, some of the user-friendliness of pattern matching was lost and it seems that further semantical investigations of inductive definitions and pattern matching are needed to throw light on the situation and on the closely related problems concerning equality in Type Theory.
The schema in did however not capture universes and some related construction needed for metamathematical applications of Type Theory. However, in it was shown that all these constructions are instances of an extended schema for a general class of simultaneous inductive-recursive definition. This seemingly fundamental constructive notions had not been isolated before. Inductive-recursive definitions are important when developing Internal Type Theory (see below) and is of interest to proof theorists studying analogues of large cardinals in Type Theory and their proof-theoretic strength.
Currently, Dybjer and Setzer are working on a finite axiomatization of inductive-recursive definitions. This axiomatization will facilitate the metatheory of induction-recursion. It has been implemented in HALF and thus provides further input to the question of how to implement inductive and recursive definitions in a proof editor.