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 This site has been updated for Coq8.2. Warning! Some solutions we propose don't work on versions prior to V8.2gamma. Please find here a tar file fully compatible with coq8.1pl3 and the printed edition of the book. These exercises were written after the release of the book (May 2004). The solution of some of them (e.g. mergesort ) illustrates new features of Coq. For instance, command Function and tactic functional induction.
HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools and pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and real analysis) to save the user work. It is also fully programmable, so users can extend it with new theorems and inference rules without compromising its soundness. There are a number of versions of HOL, going back to Mike Gordon's work in the early 80s. Compared with other HOL systems, HOL Light uses a much simpler logical core and has little legacy code, giving the system a simple and uncluttered feel. Despite its simplicity, it offers theorem proving power comparable to, and in some areas greater than, other versions of HOL, and has been used for some significant industrial-scale verification applications.