[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. Programing finger trees in Coq. In Hinze and Ramsey [10], pages 1324. http://www.lri.fr/~sozeau/research/publications/Programing_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 fourcolor theorem. Notices of the AMS, 55(11):13821393, December 2008. http://www.ams.org/notices/200811/tx081101382p.pdf. [ bib ] 
[12]  Boutheina Chetali and QuangHuy Nguyen. About the worldfirst 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.msrinria.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.epig.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.