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