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?

  • $\begingroup$ "simple, dependently-typed, inductive types": choose 2. $\endgroup$
    – cody
    Apr 1, 2014 at 22:10

2 Answers 2


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

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.


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

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

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.