<p>In addition to Martin's answer, you can try the "British school":</p>

<ul>
<li><p>Altenkirch, McBride &amp; McKinna <a href="http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf" rel="nofollow noreferrer">Why Dependent Types Matter</a></p></li>
<li><p>Goguen, McBride &amp; McKinna <a href="https://static.googleusercontent.com/media/research.google.com/en//pubs/archive/99.pdf" rel="nofollow noreferrer">Eliminating Dependent Pattern-Matching</a></p></li>
</ul>

<p>I'm sure that by this point you've been told to read Ulf Norrel's PhD dissertation. In fact pretty much any paper by Ulf is useful in this regard.</p>

CC BY-SA 4.0
2014-04-01T22:19:56.990Z
2020-04-30T22:47:40.450Z
2020-04-30T22:47:40.450Z
cody
<p>Inductive types have been studied heavily and many variants exist. A well-known introduction to inductive definitions is</p>

<ul>
<li>P. Aczel, An Introduction to Inductive Definitions</li>
</ul>

<p>which was originally published in the indispensable Handbook of Mathematical Logic, but is now available online stand-alone. An introduction to inductive types is</p>

<ul>
<li>T. Coquand, P. Dybjer, <a href="http://www.cse.chalmers.se/~peterd/papers/ESSLLI94.pdf">Inductive Definitions and Type Theory: an Introduction</a>.</li>
</ul>

<p>The theory of inductive definitions for Coq was first (?) approached in</p>

<ul>
<li>F. Pfenning, C. Paulin-Mohring, <a href="http://repository.cmu.edu/cgi/viewcontent.cgi?article=2907&amp;context=compsci">Inductively defined types in the Calculus of Constructions</a>,</li>
</ul>

<p>I don't know to what extend modern Coq has diverged from what's described in that paper. Either way, none of those is easy reading. You're probably better off to look at a Coq manual and copy the well-formedness conditions imposed there.</p>

CC BY-SA 3.0
2014-03-29T11:46:36.967Z
2014-03-29T11:46:36.967Z
Martin Berger
<p>I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. What can I read about them? Could give a simple enough well-formedness condition which I can use?</p>

CC BY-SA 3.0
2014-04-01T22:10:50.603Z
"simple, dependently-typed, inductive types": choose 2.
cody
<lo.logic><pl.programming-languages><type-theory><dependent-type>
Well-formedness condition for inductive types
Konstantin Solomatov
# Well-formedness condition for inductive types

(Asked by: username_0 on 2014-03-28)

I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. What can I read about them? Could give a simple enough well-formedness condition which I can use?

**Tags:** lo.logic, pl.programming-languages, type-theory, dependent-type

> **Comments:**
> **username_1**: "simple, dependently-typed, inductive types": choose 2.  

---

## 2 answers

### Answer by username_1 on 2014-04-01. Score: 3 | Accepted answer

In addition to Martin's answer, you can try the "British school":

* Altenkirch, McBride & McKinna [Why Dependent Types Matter](http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf)
* Goguen, McBride & McKinna [Eliminating Dependent Pattern-Matching](https://static.googleusercontent.com/media/research.google.com/en//pubs/archive/99.pdf)

I'm sure that by this point you've been told to read Ulf Norrel's PhD dissertation. In fact pretty much any paper by Ulf is useful in this regard.


---

### Answer by username_2 on 2014-03-29. Score: 6

Inductive types have been studied heavily and many variants exist. A well-known introduction to inductive definitions is

* P. Aczel, An Introduction to Inductive Definitions

which was originally published in the indispensable Handbook of Mathematical Logic, but is now available online stand-alone. An introduction to inductive types is

* T. Coquand, P. Dybjer, [Inductive Definitions and Type Theory: an Introduction](http://www.cse.chalmers.se/~peterd/papers/ESSLLI94.pdf).

The theory of inductive definitions for Coq was first (?) approached in

* F. Pfenning, C. Paulin-Mohring, [Inductively defined types in the Calculus of Constructions](http://repository.cmu.edu/cgi/viewcontent.cgi?article=2907&context=compsci),

I don't know to what extend modern Coq has diverged from what's described in that paper. Either way, none of those is easy reading. You're probably better off to look at a Coq manual and copy the well-formedness conditions imposed there.


---

