Interactive Theorem Proving and Program Development: Coq'Art: the Calculus of Inductive Constructions

Shelfclass_id 4.B.3
Sortkey BERTOT, YVES
Authors Yves Bertot, P Castâeran
Title Interactive Theorem Proving and Program Development: Coq'Art: the Calculus of Inductive Constructions
Publisher Springer-Verlag
Year c2004
Languages eng
Isbn 3540208542
Series Texts in theoretical computer science
Description xxv, 469 p. ill. 25 cm.
Record date 20071022
Location New York
Keywords Automatic theorem proving, Computer programming