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, pp 440-465.
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.
Indexed induction-recursion (with Anton Setzer). Pages 93-113 in LNCS 2183, Proof Theory in Computer Science · International Seminar, PTCS 2001 Dagstuhl Castle, Germany, October 7-12, 2001.
Induction-recursion and initial algebras (with Anton Setzer). Annals of Pure and Applied Logic 124 (2003) 1-47.
Indexed induction-recursion (with Anton Setzer). Journal of Logic and Algebraic Programming, volume 66, Issue 1 , January 2006, Pages 1-49.

Some slides

A Finite Axiomatization of Inductive-Recursive Definitions, TLCA, l'Aquila, Italy, April 1999.
Universes for Inductive and Inductive-Recursive Definitions, presented at the Uppsala-Stockholm Logic Seminar, September 2003.
The Evolution of Inductive Definitions in Type Theory (a Retrospective), lecture dedicated to Christine Paulin on the occasion of her honorary doctorate at Gothenburg University, October 2011.