APA (7th ed.) Citation

Bertot, Y., & Castéran, P. (2004). Interactive theorem proving and program development: Coq'Art : the calculus of inductive constructions. Springer.

Chicago Style (17th ed.) Citation

Bertot, Yves, and P. Castéran. Interactive Theorem Proving and Program Development: Coq'Art : The Calculus of Inductive Constructions. Berlin ; New York: Springer, 2004.

MLA (9th ed.) Citation

Bertot, Yves, and P. Castéran. Interactive Theorem Proving and Program Development: Coq'Art : The Calculus of Inductive Constructions. Springer, 2004.