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?
In addition to Martin's answer, you can try the "British school":
Altenkirch, McBride & McKinna Why Dependent Types Matter
Goguen, McBride & McKinna Eliminating Dependent Pattern-Matching
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
- T. Coquand, P. Dybjer, Inductive Definitions and Type Theory: an Introduction.
The theory of inductive definitions for Coq was first (?) approached in
- F. Pfenning, C. Paulin-Mohring, Inductively defined types in the Calculus of Constructions,
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.