Coq'Art Home page Coq'Art is the familiar name for the first book on the Coq proof assistant and its underlying theory the /Calculus of Inductive Constructions /, written by Yves Bertot and Pierre Castéran . Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions Series: Texts in Theoretical Computer Science. An EATCS Series Bertot, Yves, Castéran, Pierre 2004, XXV, 469 p., Hardcover ISBN: 3-540-20854-2 Look at Springer site . Some chapters from the book * Table of contents * A brief overview * Infinite Objects and Proofs * Foundations of Inductive Types French Version A french version of the book is available here . /Drawing "Oiseau de feu" by courtesy of Michel Mendès France/ Coq 8.1, 8.2, 8.3, 8.4, 8.5 ... The examples and solutions of exercises of the book are available as gzipped tar files : * for coq8.1pl3 * for coq8.2 * for coq8.3 * for coq 8.4 * for coq 8.5 * for coq 8.6 * for coq 8.7 * for coq 8.9 Please inform us of any problem. Sources and exercises from the book This site contains the source of all examples and the solution of 170 over 200 exercises from the book. Some new exercises are still added to this repository. For each exercise, we give a solution as a Coq file, together with some comments if the exercise is difficult, or if the solution presents some methodological interest. Comments are welcome. table of contents . *All the examples and solutions of the exercises are under licence* Cecill-B . Participation is welcome Thank you in advance for any comment, alternate solution, or any way to improve this site. Errata Some typos where found after the printing of the book. They are reported chapter by chapter, after the sources and exercises (look at this index ). Many thanks to Stefan Karrmann and Pierre Lescanne for all the remarks they sent to us. ------------------------------------------------------------------------ All (for 8.2) in a single tar file (gunzipped) All the examples and exercises on this site are copyright Yves Bertot and Pierre Castéran. Tutorial on [Co]-inductive types in Coq (V8.1 beta) Look at this page Slides for Tsinghua University Coq Summer School Click here The Teaser (draft) A set of contributions for teaching Coq (in preparation) To download Coq Coq site here ------------------------------------------------------------------------ *Mail : * /first name/./name/@labri.fr