%O Book %F coqart %A Bertot, Yves %A Castéran, Pierre %T Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions %S Texts in Theoretical Computer Science %I Springer Verlag %U http://www.labri.fr/publications/l3a/2004/BC04 %D 2004