nLab history of inductive types – references

History of inductive types

Historical references on the definition of inductive types.

Per Martin-Löf, Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions, Studies in Logic and the Foundations of Mathematics 63 (1971) 179-216 $[$ doi:10.1016/S0049-237X(08)70847-4 $]$

The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in:

Per Martin-Löf, §1.7 and p. 94 of: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 (1975) 73-118 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

and in the modern form of inference rules in:

Bengt Nordström, Kent Petersson, Jan M. Smith, §8.1 of: Programming in Martin-Löf’s Type Theory, Oxford University Press (1990) $[$ webpage, pdf, pdf $]$

The special case of inductive types now known as $\mathcal{W}$ -types is first formulated in:

Per Martin-Löf, pp. 171 of: Constructive Mathematics and Computer Programming, in: Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science (1979), Studies in Logic and the Foundations of Mathematics 104 (1982) 153-175 $[$ doi:10.1016/S0049-237X(09)70189-2, ISBN:978-0-444-85423-0 $]$
Per Martin-Löf (notes by Giovanni Sambin), Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) $[$ pdf, pdf $]$

Early proposals for a general formal definition of inductive types:

Robert L. Constable, N. Paul Francis Mendler, Recursive definitions in type theory, in Logic of Programs 1985, Lecture Notes in Computer Science 193 Springer (1985) $[$ doi:10.1007/3-540-15648-8_5 $]$
Paul Francis Mendler, Inductive Definition in Type Theory, Cornell (1987) $[$ hdl:1813/6710 $]$
Roland Backhouse, On the Meaning and Construction of the Rules of Martin-Löf’s Theory of Types, in: Workshop on General Logic, ECS-LFCS-88-52 (1988) $[$ pdf, pdf $]$

Peter Dybjer, Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, Logical frameworks (1991) 280-306 $[$ doi:10.1017/CBO9780511569807.012, pdf $]$
Peter Dybjer, Inductive families, Formal Aspects of Computing 6 (1994) 440–465 $[$ doi:10.1007/BF01211308, doi:10.1007/BF01211308, pdf $]$

and due to

Thierry Coquand, Christine Paulin, Inductively defined types, COLOG-88 Lecture Notes in Computer Science 417, Springer (1990) 50-66 $[$ doi:10.1007/3-540-52335-9_47 $]$

Frank Pfenning, Christine Paulin-Mohring, Inductively defined types in the Calculus of Constructions, in: Mathematical Foundations of Programming Semantics MFPS 1989, Lecture Notes in Computer Science 442, Springer (1990) $[$ doi:10.1007/BFb0040259 $]$
Christine Paulin-Mohring, Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) $[$ doi:10.1007/BFb0037116 $]$

reviewed in

Zhaohui Luo, §9.2.2 in: Computation and Reasoning – A Type Theory for Computer Science, Clarendon Press (1994) $[$ ISBN:9780198538356, pdf $]$
Christine Paulin-Mohring, §2.2. in: Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) $[$ hal:01094195, pdf, pdf slides $]$

with streamlined exposition in:

The generalization to inductive-recursive types is due to

Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, The Journal of Symbolic Logic 65 2 (2000) 525-549 $[$ doi:10.2307/2586554, pdf $]$
Peter Dybjer, Anton Setzer, Indexed induction-recursion, in Proof Theory in Computer Science PTCS 2001. Lecture Notes in Computer Science2183 Springer (2001) $[$ doi:10.1007/3-540-45504-3_7, pdf $]$