Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development , Coq'Art:the Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237