[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.