@book{BC04, author = {Bertot, Yves and Cast\'eran, Pierre}, title = {Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions}, year = {2004}, publisher = {Springer}, note = {\url{http://www.labri.fr/perso/casteran/CoqArt/index.html}} }

@book{piercesf2011, author = {Benjamin C. Pierce and Chris Casinghino and Michael Greenberg and Vilhelm Sj\"oberg and Brent Yorgey}, title = {Software Foundations}, publisher = {University of Pennsylvania}, year = 2011, note = {\url{http://www.cis.upenn.edu/~bcpierce/sf/}}, url = {{http://www.cis.upenn.edu/~bcpierce/sf/}} }

@book{chlipalacpdt2011, author = {Adam Chlipala}, title = {Certified Programming with Dependent Types}, publisher = {MIT Press}, year = 2011, url = {{http://adam.chlipala.net/cpdt/}}, note = {\url{http://adam.chlipala.net/cpdt/}} }

@techreport{CoqHurry, hal_id = {inria-00001173}, url = {http://cel.archives-ouvertes.fr/inria-00001173/en/}, title = {{Coq in a Hurry}}, author = {Bertot, Yves}, abstract = {{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.}}, affiliation = {MARELLE - INRIA Sophia Antipolis - INRIA}, pages = {43}, school = {Types Summer School, also used at the University of Goteborg, Nice,Ecole Jeunes Chercheurs en Programmation,Universit\'e de Nice}, year = {2010}, month = may, pdf = {\url{http://cel.archives-ouvertes.fr/inria-00001173/PDF/coq-hurry.pdf}} }

@misc{fta, author = {Herman Geuvers and Freek Wiedijk and Jan Zwanenburg and Randy Pollack and Henk Barendregt }, year = 2000, title = {The "Fundamental Theorem of Algebra" Project}, howpublished = {\url{http://www.cs.ru.nl/~freek/fta/}} }

@misc{compcert, author = {Xavier Leroy and al.}, title = {CompCert: compilers you can formally trust}, year = 2010, howpublished = {\url{http://compcert.inria.fr/}} }

@misc{Flocq, author = {Sylvie Boldo and Guillaume Melquiond}, title = {Flocq : Floats for Coq}, howpublished = {http://flocq.gforge.inria.fr/}, year = 2011 }

@inproceedings{Bolignano96ccs, author = {Dominique Bolignano}, title = {An approach to the formal verification of cryptographic protocols}, booktitle = {CCS '96 Proceedings of the 3rd ACM conference on Computer and communications security}, year = 1996 }

@inproceedings{sozeau07icfp, author = {Matthieu Sozeau}, title = {{P}rogram-ing Finger Trees in {C}oq}, pages = {13--24}, doi = {http://doi.acm.org/10.1145/1291151.1291156}, note = {\url{http://www.lri.fr/~sozeau/research/publications/Program-ing_Finger_Trees_in_Coq.pdf}}, crossref = {icfp07} }

@proceedings{icfp07, editor = {Ralf Hinze and Norman Ramsey}, title = {Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007}, booktitle = {12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007}, address = {Freiburg, Germany}, publisher = {ACM}, year = {2007}, isbn = {978-1-59593-815-2} }

@article{gonthier08ams, author = {Georges Gonthier}, title = {Formal Proof The Four-Color Theorem}, journal = {Notices of the AMS}, year = 2008, volume = 55, number = 11, pages = {1382--1393}, month = dec, note = {\url{http://www.ams.org/notices/200811/tx081101382p.pdf}} }

@misc{coqjavacardeal7, author = {Boutheina Chetali and Quang-Huy Nguyen}, title = {About the world-first smart card certificate with EAL7 formal assurances}, howpublished = {Slides 9th ICCC, Jeju, Korea}, month = sep, year = 2008, note = {\url{www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pdf}} }

@misc{certicrypt, author = {Gilles Barthe and Benjamin Gr\'egoire and Santiago Zanella and al}, title = {CertiCrypt: Formal Proofs for Computational Cryptography}, howpublished = {\url{http://www.msr-inria.inria.fr/projects/sec/certicrypt/index.html}}, annote = 2010 }

@misc{agda, author = {Catarina Coquand and Thierry Coquand and Ulf Nurell and al}, title = {Agda}, howpublished = {\url{http://wiki.portal.chalmers.se/agda}} }

@misc{prime, author = {Laurent Th\'ery and al}, title = {Certifying Prime Number with the Coq prover}, howpublished = {\url{http://coqprime.gforge.inria.fr/}}, annote = 2011 }

@misc{epigram, author = {Conor McBride and al}, title = {Epigram 2 : an experimental dependently typed functional programming language.}, howpublished = {\url{http://www.e-pig.org/darcs/Pig09/web/}} }

@misc{matita, author = {Andrea Asperti and Claudio Sacerdoti Coen and al}, title = {Matita}, howpublished = {\url{http://matita.cs.unibo.it/}} }

@misc{nuprl, author = {Robert L. Constable and Joseph L. Bates and Christoph Kreitz and Robbert van Renesse and al}, title = {PRL : Proof/Program Refinement Logic}, howpublished = {\url{http://www.cs.cornell.edu/info/projects/nuprl/}} }

*This file was generated by
bibtex2html 1.94.*