Inductive and inductive-recursive definitions in type theory
Inductive sets and families in Martin-Löf's type theory and their
set-theoretic semantics, in Logical Frameworks, 1991, editors
Gerard Huet and Gordon Plotkin, pp 280-306, Prentice Hall.
Inductive Families, in Formal Aspects of Computing 6, 1994,
- 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 15-17, 1994. Editors: P. S. Thiagarajan, Springer LNCS 880, 1994.
Representing inductively defined sets by well-orderings in
Martin-Löf's type theory. Theoretical Computer
Science 176 (1997) pp 329-335.
A general formulation of simultaneous inductive-recursive definitions in
type theory, Journal
of Symbolic Logic, Volume 65, Number 2, June 2000, pp 525-549.
A finite axiomatization of inductive-recursive definitions
(with Anton Setzer).
Pages 129 - 146 in Proceedings of TLCA 1999, LNCS 1581.
Setzer). Pages 93-113 in LNCS 2183, Proof Theory in Computer Science ·
International Seminar, PTCS 2001 Dagstuhl Castle, Germany, October
Induction-recursion and initial algebras
Setzer). Annals of Pure and
Applied Logic 124 (2003) 1-47.
Setzer). Journal of Logic and Algebraic Programming, volume 66,
Issue 1 , January 2006, Pages 1-49.