TY  - BOOK
AU  - Bertot, Yves
AU  - Casteran, Pierre
TI  - Interactive theorem proving and program development - coq' art : the calculus of inductive constructions
SN  - 9783540208549
CY  - New York
KW  - Coq  Programming language
KW  - Coq system Program development
KW  - Interactive theorem
KW  - Proofs and certified programs -- Coq
KW  - Software development
N1  - Includes bibliographical references and index
ER  -