Mercurial > cpdt > repo
changeset 310:cf67b7d6ceac
Fix .hgignore and check in .bib
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 29 Aug 2011 09:47:39 -0400 |
parents | 8cb9e31f86e7 |
children | 4cb3ba8604bc |
files | .hgignore latex/cpdt.bib |
diffstat | 2 files changed, 116 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/.hgignore Thu Aug 25 15:22:20 2011 -0400 +++ b/.hgignore Mon Aug 29 09:47:39 2011 -0400 @@ -8,7 +8,6 @@ .coq_globals */coqdoc.sty -*/cpdt.* */*.log html/coqdoc.css @@ -27,3 +26,10 @@ *.log *.tex *.toc +*.bbl +*.blg +*.idx +*.ilg +*.pdf +*.ind +*.out
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/latex/cpdt.bib Mon Aug 29 09:47:39 2011 -0400 @@ -0,0 +1,109 @@ +@Book{TAPL, + author = "Benjamin C. Pierce", + title = "Types and Programming Languages", + year = "2002", + publisher = "MIT Press" +} + +@Book{CAR, + author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore", + title = "Computer-Aided Reasoning: An Approach", + year = "2000", + publisher = "Kluwer Academic Publishers" +} + +@Article{AMD, + author = {J Strother Moore and Tom Lynch and Matt Kaufmann}, + title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm}, + journal = {IEEE Transactions on Computers}, + volume = {47(9)}, + pages = {913--926} + year = {1998} +} + +@Book{Piton, + author={J Strother Moore}, + title = {Piton: A Mechanically Verified Assembly-Level Language}, + year = "1996", + series = "Automated Reasoning Series", + publisher = "Kluwer Academic Publishers" +} + +@Article{Nqthm, + title = {The {Boyer-Moore} Theorem Prover and Its Interactive Enhancement}, + author = {Robert S. Boyer and Matt Kaufmann and J Strother Moore}, + journal = {Computers and Mathematics with Applications}, + volume = {29(2)}, + year = {1995}, + pages = {27--62} +} + +@Article{4C, + author = {Gonthier, Georges}, + year = {2008}, + title = {Formal Proof--The Four-Color Theorem}, + journal = {Notices of the American Mathematical Society}, + volume = {55(11)}, + pages = {1382-–1393} +} + +@Article{CompCert, + author = {Leroy, Xavier}, + year = {2009}, + title = {A formally verified compiler back-end}, + journal = {Journal of Automated Reasoning}, + volume = {43(4)}, + pages = {363--446} +} + +@InProceedings{seL4, + author = {Gerwin Klein + and Kevin Elphinstone + and Gernot Heiser + and June Andronick + and David Cock + and Philip Derrin + and Dhammika Elkaduwe + and Kai Engelhardt + and Rafal Kolanski + and Michael Norrish + and Thomas Sewell + and Harvey Tuch + and Simon Winwood}, + title = {{seL4}: Formal Verification of an {OS} Kernel}, + booktitle = {Proceedings of the 22nd {ACM Symposium on Operating Systems Principles}}, + year = {2009}, +} + +@Book{Isabelle/HOL, + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, + title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = 2283, + year = 2002 +} + +@Book{Isabelle, + author = {Paulson, Lawrence C.}, + year = {1994}, + title = {Isabelle: A Generic Theorem Prover}, + series = {Lecture Notes in Computer Science}, + volume = {828}, + publisher = {Springer} +} + +@Book{CoqArt, + author = "Bertot, Yves and Cast\'eran, Pierre", + title = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions", + series = "Texts in Theoretical Computer Science", + year = "2004", + publisher = "Springer Verlag", +} + +@unpublished{CoqManual, + author = "{Coq Development Team}", + title = "The {Coq} proof assistant reference manual, version 8.3", + year = 2010, + url={http://coq.inria.fr/refman/} +}