[1] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer, 2004. http://www.labri.fr/perso/casteran/CoqArt/index.html. [ bib ]
[2] Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations. University of Pennsylvania, 2011. http://www.cis.upenn.edu/~bcpierce/sf/. [ bib | www: ]
[3] Adam Chlipala. Certified Programming with Dependent Types. MIT Press, 2011. http://adam.chlipala.net/cpdt/. [ bib | www: ]
[4] Yves Bertot. Coq in a Hurry. Technical report, May 2010. [ bib | http | www: ]
These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial, so that readers can quickly start their own experiments, learning only a few of the capabilities of the system. A much more comprehensive study is provided in [1], which also provides an extensive collection of exercises to train on.

[5] Herman Geuvers, Freek Wiedijk, Jan Zwanenburg, Randy Pollack, and Henk Barendregt. The "fundamental theorem of algebra" project. http://www.cs.ru.nl/~freek/fta/, 2000. [ bib ]
[6] Xavier Leroy and al. Compcert: compilers you can formally trust. http://compcert.inria.fr/, 2010. [ bib ]
[7] Sylvie Boldo and Guillaume Melquiond. Flocq : Floats for coq. http://flocq.gforge.inria.fr/, 2011. [ bib ]
[8] Dominique Bolignano. An approach to the formal verification of cryptographic protocols. In CCS '96 Proceedings of the 3rd ACM conference on Computer and communications security, 1996. [ bib ]
[9] Matthieu Sozeau. Program-ing finger trees in Coq. In Hinze and Ramsey [10], pages 13-24. http://www.lri.fr/~sozeau/research/publications/Program-ing_Finger_Trees_in_Coq.pdf. [ bib | DOI ]
[10] Ralf Hinze and Norman Ramsey, editors. Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, 2007. ACM. [ bib ]
[11] Georges Gonthier. Formal proof the four-color theorem. Notices of the AMS, 55(11):1382-1393, December 2008. http://www.ams.org/notices/200811/tx081101382p.pdf. [ bib ]
[12] Boutheina Chetali and Quang-Huy Nguyen. About the world-first smart card certificate with eal7 formal assurances. Slides 9th ICCC, Jeju, Korea, September 2008. www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pdf. [ bib ]
[13] Gilles Barthe, Benjamin Grégoire, Santiago Zanella, and al. Certicrypt: Formal proofs for computational cryptography. http://www.msr-inria.inria.fr/projects/sec/certicrypt/index.html. [ bib ]
[14] Catarina Coquand, Thierry Coquand, Ulf Nurell, and al. Agda. http://wiki.portal.chalmers.se/agda. [ bib ]
[15] Laurent Théry and al. Certifying prime number with the coq prover. http://coqprime.gforge.inria.fr/. [ bib ]
[16] Conor McBride and al. Epigram 2 : an experimental dependently typed functional programming language. http://www.e-pig.org/darcs/Pig09/web/. [ bib ]
[17] Andrea Asperti, Claudio Sacerdoti Coen, and al. Matita. http://matita.cs.unibo.it/. [ bib ]
[18] Robert L. Constable, Joseph L. Bates, Christoph Kreitz, Robbert van Renesse, and al. Prl : Proof/program refinement logic. http://www.cs.cornell.edu/info/projects/nuprl/. [ bib ]

This file was generated by bibtex2html 1.94.