@Book{coqart, Author = {Bertot, Yves and Castéran, Pierre}, Title = {Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions}, Series = {Texts in Theoretical Computer Science}, Publisher = {Springer Verlag}, Year = {2004} }