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