Mercurial > cpdt > repo

annotate latex/cpdt.bib @ 388:057a29f9c773

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Baffling unification messages explained
author Adam Chlipala <adam@chlipala.net>
date Thu, 12 Apr 2012 16:27:28 -0400
parents 7ece04e15446
children cc8d0503619f
rev   line source
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 }
adam@387 363
adam@387 364 @inproceedings{Isar,
adam@387 365 author = {Wenzel, Markus},
adam@387 366 title = {Isar - A Generic Interpretative Approach to Readable Formal Proof Documents},
adam@387 367 booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics},
adam@387 368 series = {TPHOLs '99},
adam@387 369 year = {1999},
adam@387 370 isbn = {3-540-66463-7},
adam@387 371 pages = {167--184},
adam@387 372 numpages = {18},
adam@387 373 url = {http://dl.acm.org/citation.cfm?id=646526.694887},
adam@387 374 acmid = {694887},
adam@387 375 publisher = {Springer-Verlag},
adam@387 376 address = {London, UK, UK},
adam@387 377 }