Mercurial > cpdt > repo

comparison latex/cpdt.bib @ 310:cf67b7d6ceac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix .hgignore and check in .bib
author Adam Chlipala <adam@chlipala.net>
date Mon, 29 Aug 2011 09:47:39 -0400
parents
children 4cb3ba8604bc
comparison
equal deleted inserted replaced
309:8cb9e31f86e7 310:cf67b7d6ceac
1 @Book{TAPL,
2 author = "Benjamin C. Pierce",
3 title = "Types and Programming Languages",
4 year = "2002",
5 publisher = "MIT Press"
6 }
7
8 @Book{CAR,
9 author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore",
10 title = "Computer-Aided Reasoning: An Approach",
11 year = "2000",
12 publisher = "Kluwer Academic Publishers"
13 }
14
15 @Article{AMD,
16 author = {J Strother Moore and Tom Lynch and Matt Kaufmann},
17 title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm},
18 journal = {IEEE Transactions on Computers},
19 volume = {47(9)},
20 pages = {913--926}
21 year = {1998}
22 }
23
24 @Book{Piton,
25 author={J Strother Moore},
26 title = {Piton: A Mechanically Verified Assembly-Level Language},
27 year = "1996",
28 series = "Automated Reasoning Series",
29 publisher = "Kluwer Academic Publishers"
30 }
31
32 @Article{Nqthm,
33 title = {The {Boyer-Moore} Theorem Prover and Its Interactive Enhancement},
34 author = {Robert S. Boyer and Matt Kaufmann and J Strother Moore},
35 journal = {Computers and Mathematics with Applications},
36 volume = {29(2)},
37 year = {1995},
38 pages = {27--62}
39 }
40
41 @Article{4C,
42 author = {Gonthier, Georges},
43 year = {2008},
44 title = {Formal Proof--The Four-Color Theorem},
45 journal = {Notices of the American Mathematical Society},
46 volume = {55(11)},
47 pages = {1382-–1393}
48 }
49
50 @Article{CompCert,
51 author = {Leroy, Xavier},
52 year = {2009},
53 title = {A formally verified compiler back-end},
54 journal = {Journal of Automated Reasoning},
55 volume = {43(4)},
56 pages = {363--446}
57 }
58
59 @InProceedings{seL4,
60 author = {Gerwin Klein
61 and Kevin Elphinstone
62 and Gernot Heiser
63 and June Andronick
64 and David Cock
65 and Philip Derrin
66 and Dhammika Elkaduwe
67 and Kai Engelhardt
68 and Rafal Kolanski
69 and Michael Norrish
70 and Thomas Sewell
71 and Harvey Tuch
72 and Simon Winwood},
73 title = {{seL4}: Formal Verification of an {OS} Kernel},
74 booktitle = {Proceedings of the 22nd {ACM Symposium on Operating Systems Principles}},
75 year = {2009},
76 }
77
78 @Book{Isabelle/HOL,
79 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
80 title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
81 publisher = {Springer},
82 series = {Lecture Notes in Computer Science},
83 volume = 2283,
84 year = 2002
85 }
86
87 @Book{Isabelle,
88 author = {Paulson, Lawrence C.},
89 year = {1994},
90 title = {Isabelle: A Generic Theorem Prover},
91 series = {Lecture Notes in Computer Science},
92 volume = {828},
93 publisher = {Springer}
94 }
95
96 @Book{CoqArt,
97 author = "Bertot, Yves and Cast\'eran, Pierre",
98 title = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions",
99 series = "Texts in Theoretical Computer Science",
100 year = "2004",
101 publisher = "Springer Verlag",
102 }
103
104 @unpublished{CoqManual,
105 author = "{Coq Development Team}",
106 title = "The {Coq} proof assistant reference manual, version 8.3",
107 year = 2010,
108 url={http://coq.inria.fr/refman/}
109 }