--- 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/}
+}