|
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 }
|
|
adam@328
|
176
|
|
adam@328
|
177 @InBook{TAPLNatDed,
|
|
adam@328
|
178 author = "Benjamin C. Pierce",
|
|
adam@328
|
179 title = "Types and Programming Languages",
|
|
adam@328
|
180 year = "2002",
|
|
adam@328
|
181 publisher = "MIT Press",
|
|
adam@328
|
182 chapter = "9.4"
|
|
adam@328
|
183 }
|
|
adam@328
|
184
|
|
adam@328
|
185 @inproceedings{Monads,
|
|
adam@328
|
186 author = {Wadler, Philip},
|
|
adam@328
|
187 title = {The essence of functional programming},
|
|
adam@328
|
188 booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
|
adam@328
|
189 year = {1992},
|
|
adam@328
|
190 }
|
|
adam@328
|
191
|
|
adam@328
|
192 @inproceedings{IO,
|
|
adam@328
|
193 author = {Peyton Jones, Simon L. and Wadler, Philip},
|
|
adam@328
|
194 title = {Imperative functional programming},
|
|
adam@328
|
195 booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
|
adam@328
|
196 year = {1993},
|
|
adam@328
|
197 }
|
|
adam@328
|
198
|
|
adam@328
|
199 @InProceedings{separation,
|
|
adam@328
|
200 author = {John C. Reynolds},
|
|
adam@328
|
201 title = {Separation Logic: A Logic for Shared Mutable Data Structures},
|
|
adam@328
|
202 booktitle = {Proceedings of the IEEE Symposium on Logic in Computer Science},
|
|
adam@328
|
203 year = {2002}
|
|
adam@338
|
204 }
|
|
adam@338
|
205
|
|
adam@338
|
206 @article{Okasaki,
|
|
adam@338
|
207 author = {Okasaki, Chris},
|
|
adam@338
|
208 title = {Red-black trees in a functional setting},
|
|
adam@338
|
209 journal = {J. Funct. Program.},
|
|
adam@338
|
210 volume = {9},
|
|
adam@338
|
211 issue = {4},
|
|
adam@338
|
212 year = {1999},
|
|
adam@338
|
213 pages = {471--477},
|
|
adam@338
|
214 }
|
|
adam@342
|
215
|
|
adam@342
|
216 @Article{DeBruijn,
|
|
adam@342
|
217 author = "Nicolas G. de Bruijn",
|
|
adam@342
|
218 title = "Lambda-calculus notation with nameless dummies: a tool for automatic formal manipulation with application to the {Church-Rosser} theorem",
|
|
adam@342
|
219 journal = "Indag. Math.",
|
|
adam@342
|
220 volume = "34(5)",
|
|
adam@342
|
221 pages = "381--392",
|
|
adam@342
|
222 year = "1972"
|
|
adam@342
|
223 }
|
|
adam@343
|
224
|
|
adam@343
|
225 @INPROCEEDINGS{GirardsParadox,
|
|
adam@343
|
226 author = {Thierry Coquand},
|
|
adam@343
|
227 title = {An Analysis of {Girard's} Paradox},
|
|
adam@343
|
228 booktitle = {Proceedings of the Symposium on Logic in Computer Science},
|
|
adam@343
|
229 year = {1986},
|
|
adam@343
|
230 pages = {227--236}
|
|
adam@343
|
231 }
|
|
adam@344
|
232
|
|
adam@344
|
233 @inproceedings{PCC,
|
|
adam@344
|
234 author = {George C. Necula},
|
|
adam@344
|
235 title = {Proof-carrying code},
|
|
adam@344
|
236 booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
|
adam@344
|
237 year = {1997},
|
|
adam@344
|
238 }
|
|
adam@344
|
239
|
|
adam@344
|
240 @inproceedings{XCAP,
|
|
adam@344
|
241 author = {Ni, Zhaozhong and Shao, Zhong},
|
|
adam@344
|
242 title = {Certified assembly programming with embedded code pointers},
|
|
adam@344
|
243 booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
|
adam@344
|
244 year = {2006},
|
|
adam@344
|
245 }
|
|
adam@346
|
246
|
|
adam@346
|
247 @TechReport{IT,
|
|
adam@346
|
248 title = "A Tutorial on Recursive Types in {Coq}",
|
|
adam@346
|
249 author = "Eduardo Gim\'enez",
|
|
adam@346
|
250 year = "1998",
|
|
adam@346
|
251 month = may,
|
|
adam@346
|
252 number = "0221",
|
|
adam@346
|
253 institution = "INRIA",
|
|
adam@346
|
254 }
|
|
adam@347
|
255
|
|
adam@347
|
256 @inproceedings{BigStep,
|
|
adam@347
|
257 author = {Xavier Leroy and Herv\'e Grall},
|
|
adam@347
|
258 title = {Coinductive big-step operational semantics},
|
|
adam@347
|
259 year = {2006},
|
|
adam@347
|
260 booktitle = {Proceedings of the 15th European Symposium on Programming}
|
|
adam@347
|
261 }
|
|
adam@355
|
262
|
|
adam@355
|
263 @InBook{WinskelDomains,
|
|
adam@355
|
264 author = "Glynn Winskel",
|
|
adam@355
|
265 title = "The Formal Semantics of Programming Languages",
|
|
adam@355
|
266 year = "1993",
|
|
adam@355
|
267 publisher = "MIT Press",
|
|
adam@355
|
268 chapter = "8"
|
|
adam@355
|
269 }
|
|
adam@356
|
270
|
|
adam@356
|
271 @article{Capretta,
|
|
adam@356
|
272 author = {Venanzio Capretta},
|
|
adam@356
|
273 title = {General Recursion via Coinductive Types},
|
|
adam@356
|
274 journal = {Logical Methods in Computer Science},
|
|
adam@356
|
275 volume = 1,
|
|
adam@356
|
276 number = 2,
|
|
adam@356
|
277 year = 2005,
|
|
adam@356
|
278 pages = {1--18},
|
|
adam@356
|
279 }
|
|
adam@356
|
280
|
|
adam@356
|
281 @inproceedings{Megacz,
|
|
adam@356
|
282 author = {Adam Megacz},
|
|
adam@356
|
283 title = {A coinductive monad for prop-bounded recursion},
|
|
adam@356
|
284 booktitle = {Proceedings of the {ACM} Workshop Programming
|
|
adam@356
|
285 Languages meets Program Verification},
|
|
adam@356
|
286 pages = {11--20},
|
|
adam@356
|
287 year = {2007},
|
|
adam@356
|
288 }
|
|
adam@358
|
289
|
|
adam@358
|
290 @inproceedings{modules,
|
|
adam@358
|
291 author = {MacQueen, David},
|
|
adam@358
|
292 title = {Modules for {Standard ML}},
|
|
adam@358
|
293 booktitle = {Proceedings of the 1984 ACM Symposium on LISP and Functional Programming},
|
|
adam@358
|
294 year = {1984},
|
|
adam@358
|
295 pages = {198--207},
|
|
adam@358
|
296 }
|
|
adam@358
|
297
|
|
adam@358
|
298 @inproceedings{typeclasses,
|
|
adam@358
|
299 author = {Wadler, P. and Blott, S.},
|
|
adam@358
|
300 title = {How to make ad-hoc polymorphism less ad hoc},
|
|
adam@358
|
301 booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
|
adam@358
|
302 year = {1989},
|
|
adam@358
|
303 pages = {60--76},
|
|
adam@358
|
304 }
|
|
adam@360
|
305
|
|
adam@360
|
306 @inproceedings{reflection,
|
|
adam@360
|
307 author = {Boutin, Samuel},
|
|
adam@360
|
308 title = {Using reflection to build efficient and certified decision procedures},
|
|
adam@360
|
309 booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
|
|
adam@360
|
310 year = {1997},
|
|
adam@360
|
311 }
|
|
adam@364
|
312
|
|
adam@364
|
313 @inproceedings{JMeq,
|
|
adam@364
|
314 author = {McBride, Conor},
|
|
adam@364
|
315 title = {Elimination with a Motive},
|
|
adam@364
|
316 booktitle = {Proceedings of the International Workshop on Types for Proofs and Programs},
|
|
adam@364
|
317 year = {2000},
|
|
adam@364
|
318 pages = {197--216}
|
|
adam@364
|
319 }
|
|
adam@364
|
320
|
|
adam@364
|
321 @phdthesis{AxiomK,
|
|
adam@364
|
322 author = {Thomas Streicher},
|
|
adam@364
|
323 title = {Semantical Investigations into Intensional Type Theory},
|
|
adam@364
|
324 type = {Habilitationsschrift},
|
|
adam@364
|
325 school = {LMU M\"unchen},
|
|
adam@364
|
326 year= {1993}
|
|
adam@364
|
327 }
|
|
adam@381
|
328
|
|
adam@381
|
329 @article{BGB,
|
|
adam@381
|
330 author = {Geoffrey Washburn and Stephanie Weirich},
|
|
adam@381
|
331 title = {Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism},
|
|
adam@381
|
332 journal = {J. Funct. Program.},
|
|
adam@381
|
333 volume = {18},
|
|
adam@381
|
334 number = {1},
|
|
adam@381
|
335 year = {2008},
|
|
adam@381
|
336 pages = {87--140},
|
|
adam@381
|
337 publisher = {Cambridge University Press},
|
|
adam@381
|
338 address = {New York, NY, USA},
|
|
adam@381
|
339 }
|
|
adam@381
|
340
|
|
adam@381
|
341 @InProceedings{PhoasICFP08,
|
|
adam@381
|
342 author = {Adam Chlipala},
|
|
adam@381
|
343 title = {Parametric Higher-Order Abstract Syntax for Mechanized Semantics},
|
|
adam@381
|
344 booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming},
|
|
adam@381
|
345 year = {2008},
|
|
adam@381
|
346 pages = {143--156}
|
|
adam@381
|
347 }
|
|
adam@381
|
348
|
|
adam@381
|
349 @article{parametricity,
|
|
adam@381
|
350 author = {Reynolds, J.C.},
|
|
adam@381
|
351 year = {1983},
|
|
adam@381
|
352 title = {Types, abstraction, and parametric polymorphism},
|
|
adam@381
|
353 journal = {Information Processing},
|
|
adam@381
|
354 pages = {513--523}
|
|
adam@381
|
355 }
|
|
adam@381
|
356
|
|
adam@381
|
357 @InProceedings{CompilerPOPL10,
|
|
adam@381
|
358 author = {Adam Chlipala},
|
|
adam@381
|
359 title = {A Verified Compiler for an Impure Functional Language},
|
|
adam@381
|
360 booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
|
adam@381
|
361 year = {2010},
|
|
adam@381
|
362 }
|
