Bertot, Y., & Castéran, P. [ca. 2004]. Interactive theorem proving and program development : Coq’Art: the calculus of inductive constructions. In Texts in theoretical computer science [Book]. Berlin [u.a.]: Springer.

BERTOT, Yves und CASTÉRAN, Pierre, 2004. Interactive theorem proving and program development : Coq’Art: the calculus of inductive constructions. Berlin [u.a.]: Springer. ISBN 9783642058806.

Bertot, Y., und P. Castéran. „Interactive theorem proving and program development : Coq’Art: the calculus of inductive constructions“. Texts in theoretical computer science, book, Springer, 2004.

Bertot, Yves/Castéran, Pierre: Interactive theorem proving and program development : Coq’Art: the calculus of inductive constructions, Berlin [u.a.] 2004.

Bertot, Y. und Castéran, P. (2004), Interactive theorem proving and program development : Coq’Art: the calculus of inductive constructions, Texts in theoretical computer science, Bd. , Springer, Berlin [u.a.].