Mercurial > cpdt > repo

comparison latex/cpdt.bib @ 510:fd6ec9b2dccb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finished last pass through the book before beginning the MIT Press editorial process
author Adam Chlipala <adam@chlipala.net>
date Wed, 13 Feb 2013 10:22:18 -0500
parents e53d051681b0
children
comparison
equal deleted inserted replaced
509:21079e42b773 510:fd6ec9b2dccb
71 and Harvey Tuch 71 and Harvey Tuch
72 and Simon Winwood}, 72 and Simon Winwood},
73 title = {{seL4}: Formal Verification of an {OS} Kernel}, 73 title = {{seL4}: Formal Verification of an {OS} Kernel},
74 booktitle = {Proceedings of the 22nd {ACM Symposium on Operating Systems Principles}}, 74 booktitle = {Proceedings of the 22nd {ACM Symposium on Operating Systems Principles}},
75 year = {2009}, 75 year = {2009},
76 pages = {207--220}
76 } 77 }
77 78
78 @Book{Isabelle/HOL, 79 @Book{Isabelle/HOL,
79 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, 80 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
80 title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, 81 title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
111 @inproceedings{CIC, 112 @inproceedings{CIC,
112 author = {Christine Paulin-Mohring}, 113 author = {Christine Paulin-Mohring},
113 title = {Inductive Definitions in the System {Coq} - Rules and Properties}, 114 title = {Inductive Definitions in the System {Coq} - Rules and Properties},
114 year = {1993}, 115 year = {1993},
115 booktitle = {Proceedings of the International Conference on {Typed Lambda Calculi and Applications}}, 116 booktitle = {Proceedings of the International Conference on {Typed Lambda Calculi and Applications}},
117 pages = {328--345}
116 } 118 }
117 119
118 @inproceedings{SetsInTypes, 120 @inproceedings{SetsInTypes,
119 author = {Benjamin Werner}, 121 author = {Benjamin Werner},
120 title = {Sets in Types, Types in Sets}, 122 title = {Sets in Types, Types in Sets},
121 booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software}, 123 booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
122 year = {1997}, 124 year = {1997},
125 pages = {530--546}
123 } 126 }
124 127
125 @article{CoC, 128 @article{CoC,
126 author = {Thierry Coquand and G\'erard Huet}, 129 author = {Thierry Coquand and G\'erard Huet},
127 title = {The {Calculus} of {Constructions}}, 130 title = {The {Calculus} of {Constructions}},
131 } 134 }
132 135
133 @inproceedings{GADT, 136 @inproceedings{GADT,
134 author = {Hongwei Xi and Chiyan Chen and Gang Chen}, 137 author = {Hongwei Xi and Chiyan Chen and Gang Chen},
135 title = {Guarded Recursive Datatype Constructors}, 138 title = {Guarded Recursive Datatype Constructors},
136 booktitle = {Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages}, 139 booktitle = {Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
137 year = {2003} 140 year = {2003},
141 pages = {224--235}
138 } 142 }
139 143
140 @article{Curry, 144 @article{Curry,
141 title={Functionality in Combinatory Logic}, 145 title={Functionality in Combinatory Logic},
142 author = {H. B. Curry}, 146 author = {H. B. Curry},
160 @inproceedings{HOAS, 164 @inproceedings{HOAS,
161 author = {Pfenning, F. and Elliot, C.}, 165 author = {Pfenning, F. and Elliot, C.},
162 title = {Higher-order abstract syntax}, 166 title = {Higher-order abstract syntax},
163 booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation}, 167 booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation},
164 year = {1988}, 168 year = {1988},
165 % pages = {199--208}, 169 pages = {199--208}
166 } 170 }
167 171
168 @article{HOU, 172 @article{HOU,
169 author = {G\'erard Huet}, 173 author = {G\'erard Huet},
170 title = {The undecidability of unification in third order logic}, 174 title = {The undecidability of unification in third order logic},
185 @inproceedings{Monads, 189 @inproceedings{Monads,
186 author = {Wadler, Philip}, 190 author = {Wadler, Philip},
187 title = {The essence of functional programming}, 191 title = {The essence of functional programming},
188 booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, 192 booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
189 year = {1992}, 193 year = {1992},
194 pages = {1--14}
190 } 195 }
191 196
192 @inproceedings{IO, 197 @inproceedings{IO,
193 author = {Peyton Jones, Simon L. and Wadler, Philip}, 198 author = {Peyton Jones, Simon L. and Wadler, Philip},
194 title = {Imperative functional programming}, 199 title = {Imperative functional programming},
195 booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, 200 booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
196 year = {1993}, 201 year = {1993},
202 pages = {71--84}
197 } 203 }
198 204
199 @InProceedings{separation, 205 @InProceedings{separation,
200 author = {John C. Reynolds}, 206 author = {John C. Reynolds},
201 title = {Separation Logic: A Logic for Shared Mutable Data Structures}, 207 title = {Separation Logic: A Logic for Shared Mutable Data Structures},
202 booktitle = {Proceedings of the IEEE Symposium on Logic in Computer Science}, 208 booktitle = {Proceedings of the IEEE Symposium on Logic in Computer Science},
203 year = {2002} 209 year = {2002},
210 pages = {55--74}
204 } 211 }
205 212
206 @article{Okasaki, 213 @article{Okasaki,
207 author = {Okasaki, Chris}, 214 author = {Okasaki, Chris},
208 title = {Red-black trees in a functional setting}, 215 title = {Red-black trees in a functional setting},
233 @inproceedings{PCC, 240 @inproceedings{PCC,
234 author = {George C. Necula}, 241 author = {George C. Necula},
235 title = {Proof-carrying code}, 242 title = {Proof-carrying code},
236 booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, 243 booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
237 year = {1997}, 244 year = {1997},
245 pages = {106--119}
238 } 246 }
239 247
240 @inproceedings{XCAP, 248 @inproceedings{XCAP,
241 author = {Ni, Zhaozhong and Shao, Zhong}, 249 author = {Ni, Zhaozhong and Shao, Zhong},
242 title = {Certified assembly programming with embedded code pointers}, 250 title = {Certified assembly programming with embedded code pointers},
243 booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, 251 booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
244 year = {2006}, 252 year = {2006},
253 pages = {320--333}
245 } 254 }
246 255
247 @TechReport{IT, 256 @TechReport{IT,
248 title = "A Tutorial on Recursive Types in {Coq}", 257 title = "A Tutorial on Recursive Types in {Coq}",
249 author = "Eduardo Gim\'enez", 258 author = "Eduardo Gim\'enez",
255 264
256 @inproceedings{BigStep, 265 @inproceedings{BigStep,
257 author = {Xavier Leroy and Herv\'e Grall}, 266 author = {Xavier Leroy and Herv\'e Grall},
258 title = {Coinductive big-step operational semantics}, 267 title = {Coinductive big-step operational semantics},
259 year = {2006}, 268 year = {2006},
260 booktitle = {Proceedings of the 15th European Symposium on Programming} 269 booktitle = {Proceedings of the 15th European Symposium on Programming},
270 pages = {54--68}
261 } 271 }
262 272
263 @InBook{WinskelDomains, 273 @InBook{WinskelDomains,
264 author = "Glynn Winskel", 274 author = "Glynn Winskel",
265 title = "The Formal Semantics of Programming Languages", 275 title = "The Formal Semantics of Programming Languages",
298 @inproceedings{typeclasses, 308 @inproceedings{typeclasses,
299 author = {Wadler, P. and Blott, S.}, 309 author = {Wadler, P. and Blott, S.},
300 title = {How to make ad-hoc polymorphism less ad hoc}, 310 title = {How to make ad-hoc polymorphism less ad hoc},
301 booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, 311 booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
302 year = {1989}, 312 year = {1989},
303 % pages = {60--76}, 313 pages = {60--76}
304 } 314 }
305 315
306 @inproceedings{reflection, 316 @inproceedings{reflection,
307 author = {Boutin, Samuel}, 317 author = {Boutin, Samuel},
308 title = {Using reflection to build efficient and certified decision procedures}, 318 title = {Using reflection to build efficient and certified decision procedures},
309 booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software}, 319 booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
310 year = {1997}, 320 year = {1997},
321 pages = {515--529}
311 } 322 }
312 323
313 @inproceedings{JMeq, 324 @inproceedings{JMeq,
314 author = {McBride, Conor}, 325 author = {McBride, Conor},
315 title = {Elimination with a Motive}, 326 title = {Elimination with a Motive},
357 @InProceedings{CompilerPOPL10, 368 @InProceedings{CompilerPOPL10,
358 author = {Adam Chlipala}, 369 author = {Adam Chlipala},
359 title = {A Verified Compiler for an Impure Functional Language}, 370 title = {A Verified Compiler for an Impure Functional Language},
360 booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, 371 booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
361 year = {2010}, 372 year = {2010},
373 pages = {93--106}
362 } 374 }
363 375
364 @inproceedings{Isar, 376 @inproceedings{Isar,
365 author = {Wenzel, Markus}, 377 author = {Wenzel, Markus},
366 title = {Isar - A Generic Interpretative Approach to Readable Formal Proof Documents}, 378 title = {Isar - A Generic Interpretative Approach to Readable Formal Proof Documents},
367 booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics}, 379 booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics},
368 year = {1999}, 380 year = {1999},
381 pages = {167--184}
369 } 382 }
370 383
371 @article{continuations, 384 @article{continuations,
372 author = {Reynolds, John C.}, 385 author = {Reynolds, John C.},
373 title = {The discoveries of continuations}, 386 title = {The discoveries of continuations},