|||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 ]|
|||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: ]|
|||Adam Chlipala. Certified Programming with Dependent Types. MIT Press, 2011. http://adam.chlipala.net/cpdt/. [ bib | www: ]|
Coq in a Hurry.
Technical report, May 2010.
[ bib |
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 , which also provides an extensive collection of exercises to train on.
|||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 ]|
|||Xavier Leroy and al. Compcert: compilers you can formally trust. http://compcert.inria.fr/, 2010. [ bib ]|
|||Sylvie Boldo and Guillaume Melquiond. Flocq : Floats for coq. http://flocq.gforge.inria.fr/, 2011. [ bib ]|
|||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 ]|
|||Matthieu Sozeau. Program-ing finger trees in Coq. In Hinze and Ramsey , pages 13-24. http://www.lri.fr/~sozeau/research/publications/Program-ing_Finger_Trees_in_Coq.pdf. [ bib | DOI ]|
|||Ralf Hinze and Norman Ramsey, editors. Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, 2007. ACM. [ bib ]|
|||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 ]|
|||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 ]|
|||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 ]|
|||Catarina Coquand, Thierry Coquand, Ulf Nurell, and al. Agda. http://wiki.portal.chalmers.se/agda. [ bib ]|
|||Laurent Théry and al. Certifying prime number with the coq prover. http://coqprime.gforge.inria.fr/. [ bib ]|
|||Conor McBride and al. Epigram 2 : an experimental dependently typed functional programming language. http://www.e-pig.org/darcs/Pig09/web/. [ bib ]|
|||Andrea Asperti, Claudio Sacerdoti Coen, and al. Matita. http://matita.cs.unibo.it/. [ bib ]|
|||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.