|
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 }
|
|
adam@311
|
110
|
|
adam@311
|
111 @inproceedings{CIC,
|
|
adam@311
|
112 author = {Christine Paulin-Mohring},
|
|
adam@311
|
113 title = {Inductive Definitions in the System {Coq} - Rules and Properties},
|
|
adam@311
|
114 year = {1993},
|
|
adam@311
|
115 booktitle = {Proceedings of the International Conference on {Typed Lambda Calculi and Applications}},
|
|
adam@311
|
116 }
|
|
adam@311
|
117
|
|
adam@311
|
118 @inproceedings{SetsInTypes,
|
|
adam@311
|
119 author = {Benjamin Werner},
|
|
adam@311
|
120 title = {Sets in Types, Types in Sets},
|
|
adam@311
|
121 booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
|
|
adam@311
|
122 year = {1997},
|
|
adam@311
|
123 }
|
|
adam@311
|
124
|
|
adam@311
|
125 @article{CoC,
|
|
adam@311
|
126 author = {Thierry Coquand and G\'erard Huet},
|
|
adam@311
|
127 title = {The {Calculus} of {Constructions}},
|
|
adam@311
|
128 journal = {Information and Computation},
|
|
adam@311
|
129 volume = {76(2-3)},
|
|
adam@311
|
130 year = {1988}
|
|
adam@311
|
131 }
|
|
adam@312
|
132
|
|
adam@315
|
133 @inproceedings{GADT,
|
|
adam@312
|
134 author = {Hongwei Xi and Chiyan Chen and Gang Chen},
|
|
adam@312
|
135 title = {Guarded Recursive Datatype Constructors},
|
|
adam@312
|
136 booktitle = {Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages},
|
|
adam@312
|
137 year = {2003}
|
|
adam@312
|
138 }
|
|
adam@315
|
139
|
|
adam@315
|
140 @article{Curry,
|
|
adam@315
|
141 title={Functionality in Combinatory Logic},
|
|
adam@315
|
142 author = {H. B. Curry},
|
|
adam@315
|
143 journal = {Proceedings of the National Academy of Sciences of the United States of America},
|
|
adam@315
|
144 volume = {20(11)},
|
|
adam@315
|
145 year = {1934},
|
|
adam@315
|
146 pages = {584--590}
|
|
adam@315
|
147 }
|
|
adam@315
|
148
|
|
adam@315
|
149 @incollection{Howard,
|
|
adam@315
|
150 author = {Howard, William A.},
|
|
adam@315
|
151 title = {The formulae-as-types notion of construction},
|
|
adam@315
|
152 editor = {Seldin, Jonathan P. and Hindley, J. Roger},
|
|
adam@315
|
153 booktitle = {To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
|
|
adam@315
|
154 publisher = {Academic Press},
|
|
adam@315
|
155 pages = {479--490},
|
|
adam@315
|
156 year = {1980},
|
|
adam@315
|
157 note = {Original paper manuscript from 1969}
|
|
adam@315
|
158 }
|
|
adam@316
|
159
|
|
adam@316
|
160 @inproceedings{HOAS,
|
|
adam@316
|
161 author = {Pfenning, F. and Elliot, C.},
|
|
adam@316
|
162 title = {Higher-order abstract syntax},
|
|
adam@316
|
163 booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation},
|
|
adam@316
|
164 year = {1988},
|
|
adam@316
|
165 pages = {199--208},
|
|
adam@316
|
166 }
|
|
adam@317
|
167
|
|
adam@317
|
168 @article{HOU,
|
|
adam@317
|
169 author = {G\'erard Huet},
|
|
adam@317
|
170 title = {The undecidability of unification in third order logic},
|
|
adam@317
|
171 journal = {Information and Control},
|
|
adam@317
|
172 voluem = {22(3)},
|
|
adam@317
|
173 year = {1973},
|
|
adam@317
|
174 pages = {257--267}
|
|
adam@317
|
175 }
|
