Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeJan 3rd 2023
   • (edited Jan 3rd 2023)
   • PermaLink
   Author: Urs
   Format: MarkdownItexa bare list of references, to be `!include`-ed into the References-lists of relevant entries (*[[inductive type]]*, *[[inductive familiy]]*, *[[inductive-recursive family]]*, *[[calculus of inductive constructions]]*) this list includes a polished-up version of * all the references previously listed at *[[inductive familiy]]* in the section "History" (due to [revisions $\leq 5$](https://ncatlab.org/nlab/revision/diff/inductive+family/5) by Bas Spitters) * further references previously listed at *[[inductive-recursive type]]* and some more <a href="https://ncatlab.org/nlab/revision/history+of+inductive+types+--+references/1">v1</a>, <a href="https://ncatlab.org/nlab/show/history+of+inductive+types+--+references">current</a>

   a bare list of references, to be !include-ed into the References-lists of relevant entries (inductive type, inductive familiy, inductive-recursive family, calculus of inductive constructions)

   this list includes a polished-up version of

   • all the references previously listed at inductive familiy in the section “History” (due to revisions $\leq 5$ by Bas Spitters)

   • further references previously listed at inductive-recursive type

   and some more

   v1, current

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeJan 17th 2023
   • PermaLink
   Author: Urs
   Format: MarkdownItexadded pointer to: * [[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](https://doi.org/10.1007/3-540-15648-8_5)$]$ <a href="https://ncatlab.org/nlab/revision/diff/history+of+inductive+types+--+references/3">diff</a>, <a href="https://ncatlab.org/nlab/revision/history+of+inductive+types+--+references/3">v3</a>, <a href="https://ncatlab.org/nlab/show/history+of+inductive+types+--+references">current</a>

   added pointer to:

   • 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$]$

   diff, v3, current

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeJan 17th 2023
   • PermaLink
   Author: Urs
   Format: MarkdownItexand pointer to: * [[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](https://doi.org/10.1007/BFb0040259)$]$ <a href="https://ncatlab.org/nlab/revision/diff/history+of+inductive+types+--+references/3">diff</a>, <a href="https://ncatlab.org/nlab/revision/history+of+inductive+types+--+references/3">v3</a>, <a href="https://ncatlab.org/nlab/show/history+of+inductive+types+--+references">current</a>

   and pointer to:

   • 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$]$

   diff, v3, current

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeMay 18th 2023
   • PermaLink
   Author: Urs
   Format: MarkdownItexadded earlier reference for the introduction of the notion of W-types: * [[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 $[$<a href="https://doi.org/10.1016/S0049-237X(09)70189-2">doi:10.1016/S0049-237X(09)70189-2</a>, [ISBN:978-0-444-85423-0](https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/104/suppl/C)$]$ following a hint in another thread ([here](https://nforum.ncatlab.org/discussion/3464/inductive-type/?Focus=109587#Comment_109587)) <a href="https://ncatlab.org/nlab/revision/diff/history+of+inductive+types+--+references/4">diff</a>, <a href="https://ncatlab.org/nlab/revision/history+of+inductive+types+--+references/4">v4</a>, <a href="https://ncatlab.org/nlab/show/history+of+inductive+types+--+references">current</a>

   added earlier reference for the introduction of the notion of W-types:

   • 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$]$

   following a hint in another thread (here)

   diff, v4, current

5. • CommentRowNumber5.
   • CommentAuthornLab edit announcer
   • CommentTime1 day ago
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexcorrect link which pointed to a different paper than claimed Evan Cavallo <a href="https://ncatlab.org/nlab/revision/diff/history+of+inductive+types+--+references/5">diff</a>, <a href="https://ncatlab.org/nlab/revision/history+of+inductive+types+--+references/5">v5</a>, <a href="https://ncatlab.org/nlab/show/history+of+inductive+types+--+references">current</a>

   correct link which pointed to a different paper than claimed

   Evan Cavallo

   diff, v5, current

6. • CommentRowNumber6.
   • CommentAuthorvarkor
   • CommentTime3 hours ago
   • PermaLink
   Author: varkor
   Format: MarkdownItexChange a double hyphen to an en-dash. <a href="https://ncatlab.org/nlab/revision/diff/history+of+inductive+types+%E2%80%93+references/6">diff</a>, <a href="https://ncatlab.org/nlab/revision/history+of+inductive+types+%E2%80%93+references/6">v6</a>, <a href="https://ncatlab.org/nlab/show/history+of+inductive+types+%E2%80%93+references">current</a>

   Change a double hyphen to an en-dash.

   diff, v6, current