Inductive and inductiverecursive definitions in type theory

Inductive sets and families in MartinLöf's type theory and their
settheoretic semantics, in Logical Frameworks, 1991, editors
Gerard Huet and Gordon Plotkin, pp 280306, Prentice Hall.

Inductive Families, in Formal Aspects of Computing 6, 1994,
pp 440465.
 Inductive Definitions and Type Theory. Lecture notes for ESSLLI'94, Copenhagen. Revised form appeared as
Inductive definitions and type theory an introduction (preliminary version) (with Thierry Coquand), pp 60  76 in
Foundation of Software Technology and Theoretical Computer Science: 14th Conference Madras, India, December 1517, 1994. Editors: P. S. Thiagarajan, Springer LNCS 880, 1994.

Representing inductively defined sets by wellorderings in
MartinLöf's type theory. Theoretical Computer
Science 176 (1997) pp 329335.

A general formulation of simultaneous inductiverecursive definitions in
type theory, Journal
of Symbolic Logic, Volume 65, Number 2, June 2000, pp 525549.

A finite axiomatization of inductiverecursive definitions
(with Anton Setzer).
Pages 129  146 in Proceedings of TLCA 1999, LNCS 1581.

Indexed inductionrecursion
(with Anton
Setzer). Pages 93113 in LNCS 2183, Proof Theory in Computer Science ·
International Seminar, PTCS 2001 Dagstuhl Castle, Germany, October
712, 2001.

Inductionrecursion and initial algebras
(with Anton
Setzer). Annals of Pure and
Applied Logic 124 (2003) 147.

Indexed inductionrecursion
(with Anton
Setzer). Journal of Logic and Algebraic Programming, volume 66,
Issue 1 , January 2006, Pages 149.
Some slides