The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT loria.fr>]

On Tue, 8 Mar 2005, Lionel Elie Mamane wrote:

> canonical reference for the notion is:
>
> Peter Dybjer, A general formulation of simultaneous
> inductive-recursive definitions in type theory, Journal of Symbolic
> Logic, 65(2), June 2000.

you can also have a look at:

Inductive types in the Calculus of Algebraic Constructions,
to appear in Fundamenta Informaticae
see http://www.loria.fr/~blanqui/

> Notice the relatively recent date :-) But maybe someone will correct
> me and say that the notion was known for longer.

i think so, even though it was not called like this. peter himself gives 
examples of such definitions in martin-lof's work.