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