Mercurial > cpdt > repo

annotate latex/cpdt.bib @ 451:822442bf6d7f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proofreading pass through Chapter 5
author Adam Chlipala <adam@chlipala.net>
date Fri, 17 Aug 2012 15:39:55 -0400
parents 92f386c33e94
children e53d051681b0
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@434 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@434 106 title = "The {Coq} proof assistant reference manual, version 8.4",
adam@434 107 year = 2012,
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 year = {1999},
adam@387 369 }
adam@394 370
adam@394 371 @article{continuations,
adam@394 372 author = {Reynolds, John C.},
adam@394 373 title = {The discoveries of continuations},
adam@394 374 journal = {Lisp Symb. Comput.},
adam@394 375 issue_date = {Nov. 1993},
adam@394 376 volume = {6},
adam@394 377 number = {3-4},
adam@394 378 month = nov,
adam@394 379 year = {1993},
adam@394 380 issn = {0892-4635},
adam@394 381 pages = {233--248},
adam@394 382 numpages = {16},
adam@394 383 url = {http://dx.doi.org/10.1007/BF01019459},
adam@394 384 doi = {10.1007/BF01019459},
adam@394 385 acmid = {198114},
adam@394 386 publisher = {Kluwer Academic Publishers},
adam@394 387 address = {Hingham, MA, USA},
adam@394 388 keywords = {continuation, continuation-passing style, semantics},
adam@394 389 }
adam@394 390
adam@394 391 @article{unification,
adam@394 392 author = {Robinson, J. A.},
adam@394 393 title = {A Machine-Oriented Logic Based on the Resolution Principle},
adam@394 394 journal = {J. ACM},
adam@394 395 issue_date = {Jan. 1965},
adam@394 396 volume = {12},
adam@394 397 number = {1},
adam@394 398 month = jan,
adam@394 399 year = {1965},
adam@394 400 issn = {0004-5411},
adam@394 401 pages = {23--41},
adam@394 402 numpages = {19},
adam@394 403 url = {http://doi.acm.org/10.1145/321250.321253},
adam@394 404 doi = {10.1145/321250.321253},
adam@394 405 acmid = {321253},
adam@394 406 publisher = {ACM},
adam@394 407 address = {New York, NY, USA},
adam@394 408 }
adam@395 409
adam@395 410 @ARTICLE{whyfp,
adam@395 411 author = {John Hughes},
adam@395 412 title = {Why Functional Programming Matters},
adam@395 413 journal = {The Computer Journal},
adam@395 414 year = {1984},
adam@395 415 volume = {32},
adam@395 416 pages = {98--107}
adam@395 417 }
adam@395 418
adam@395 419 @Book{Prolog,
adam@395 420 author = "Leon Sterling and Ehud Shapiro",
adam@395 421 title = "The Art of Prolog, 2nd Edition",
adam@395 422 year = "1994",
adam@395 423 publisher = "MIT Press"
adam@395 424 }
adam@395 425
adam@395 426 @Book{LogicProgramming,
adam@395 427 author = "John W. Lloyd",
adam@395 428 title = "Foundations of Logic Programming, 2nd Edition",
adam@395 429 year = "1987",
adam@395 430 publisher = "Springer"
adam@395 431 }
adam@395 432
adam@395 433 @InBook{deriving,
adam@395 434 title = "Haskell 98 Language and Libraries: The Revised Report",
adam@395 435 author = "Simon {Peyton Jones} and Lennart Augustsson and Dave Barton and Brian Boutel and Warren Burton and Joseph Fasel and Kevin Hammond and Ralf Hinze and Paul Hudak and John Hughes and Thomas Johnsson and Mark Jones and John Launchbury and Erik Meijer and John Peterson and Alastair Reid and Colin Runciman and Philip Wadler",
adam@395 436 year = "1998",
adam@395 437 chapter = "4.3.3",
adam@395 438 url = {http://www.haskell.org/onlinereport/decls.html#derived-decls}
adam@395 439 }