Bertot, Yves <br/><br/>
Interactive theorem proving and program development - coq' art : the calculus of inductive constructions 

 - New York  Springer  2004 
 - xxv, 469p.   
<br/><br/> Includes bibliographical references and index 
<br/><br/><label>ISBN: </label>9783540208549 
<br/><br/><label>Subjects--Topical Terms: </label><br/>Coq  Programming language<br/>Coq system Program development<br/>Interactive theorem<br/>Proofs and certified programs -- Coq<br/>Software development