Mercurial > cpdt > repo

annotate latex/cpdt.bib @ 569:0ce9829efa3b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Back to working in Coq 8.4
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Jan 2019 15:28:23 -0500
parents fd6ec9b2dccb
children
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@464 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@510 76 pages = {207--220}
adam@310 77 }
adam@310 78
adam@310 79 @Book{Isabelle/HOL,
adam@310 80 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
adam@310 81 title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
adam@310 82 publisher = {Springer},
adam@310 83 series = {Lecture Notes in Computer Science},
adam@310 84 volume = 2283,
adam@310 85 year = 2002
adam@310 86 }
adam@310 87
adam@310 88 @Book{Isabelle,
adam@310 89 author = {Paulson, Lawrence C.},
adam@310 90 year = {1994},
adam@310 91 title = {Isabelle: A Generic Theorem Prover},
adam@310 92 series = {Lecture Notes in Computer Science},
adam@310 93 volume = {828},
adam@310 94 publisher = {Springer}
adam@310 95 }
adam@310 96
adam@310 97 @Book{CoqArt,
adam@310 98 author = "Bertot, Yves and Cast\'eran, Pierre",
adam@310 99 title = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions",
adam@310 100 series = "Texts in Theoretical Computer Science",
adam@310 101 year = "2004",
adam@310 102 publisher = "Springer Verlag",
adam@310 103 }
adam@310 104
adam@310 105 @unpublished{CoqManual,
adam@310 106 author = "{Coq Development Team}",
adam@434 107 title = "The {Coq} proof assistant reference manual, version 8.4",
adam@434 108 year = 2012,
adam@310 109 url={http://coq.inria.fr/refman/}
adam@310 110 }
adam@311 111
adam@311 112 @inproceedings{CIC,
adam@311 113 author = {Christine Paulin-Mohring},
adam@311 114 title = {Inductive Definitions in the System {Coq} - Rules and Properties},
adam@311 115 year = {1993},
adam@311 116 booktitle = {Proceedings of the International Conference on {Typed Lambda Calculi and Applications}},
adam@510 117 pages = {328--345}
adam@311 118 }
adam@311 119
adam@311 120 @inproceedings{SetsInTypes,
adam@311 121 author = {Benjamin Werner},
adam@311 122 title = {Sets in Types, Types in Sets},
adam@311 123 booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
adam@311 124 year = {1997},
adam@510 125 pages = {530--546}
adam@311 126 }
adam@311 127
adam@311 128 @article{CoC,
adam@311 129 author = {Thierry Coquand and G\'erard Huet},
adam@311 130 title = {The {Calculus} of {Constructions}},
adam@311 131 journal = {Information and Computation},
adam@311 132 volume = {76(2-3)},
adam@311 133 year = {1988}
adam@311 134 }
adam@312 135
adam@315 136 @inproceedings{GADT,
adam@312 137 author = {Hongwei Xi and Chiyan Chen and Gang Chen},
adam@312 138 title = {Guarded Recursive Datatype Constructors},
adam@510 139 booktitle = {Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
adam@510 140 year = {2003},
adam@510 141 pages = {224--235}
adam@312 142 }
adam@315 143
adam@315 144 @article{Curry,
adam@315 145 title={Functionality in Combinatory Logic},
adam@315 146 author = {H. B. Curry},
adam@315 147 journal = {Proceedings of the National Academy of Sciences of the United States of America},
adam@315 148 volume = {20(11)},
adam@315 149 year = {1934},
adam@315 150 pages = {584--590}
adam@315 151 }
adam@315 152
adam@315 153 @incollection{Howard,
adam@315 154 author = {Howard, William A.},
adam@315 155 title = {The formulae-as-types notion of construction},
adam@315 156 editor = {Seldin, Jonathan P. and Hindley, J. Roger},
adam@315 157 booktitle = {To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
adam@315 158 publisher = {Academic Press},
adam@315 159 pages = {479--490},
adam@315 160 year = {1980},
adam@315 161 note = {Original paper manuscript from 1969}
adam@315 162 }
adam@316 163
adam@316 164 @inproceedings{HOAS,
adam@316 165 author = {Pfenning, F. and Elliot, C.},
adam@316 166 title = {Higher-order abstract syntax},
adam@316 167 booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation},
adam@316 168 year = {1988},
adam@510 169 pages = {199--208}
adam@316 170 }
adam@317 171
adam@317 172 @article{HOU,
adam@317 173 author = {G\'erard Huet},
adam@317 174 title = {The undecidability of unification in third order logic},
adam@317 175 journal = {Information and Control},
adam@317 176 voluem = {22(3)},
adam@317 177 year = {1973},
adam@317 178 pages = {257--267}
adam@317 179 }
adam@328 180
adam@328 181 @InBook{TAPLNatDed,
adam@328 182 author = "Benjamin C. Pierce",
adam@328 183 title = "Types and Programming Languages",
adam@328 184 year = "2002",
adam@328 185 publisher = "MIT Press",
adam@328 186 chapter = "9.4"
adam@328 187 }
adam@328 188
adam@328 189 @inproceedings{Monads,
adam@328 190 author = {Wadler, Philip},
adam@328 191 title = {The essence of functional programming},
adam@328 192 booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
adam@328 193 year = {1992},
adam@510 194 pages = {1--14}
adam@328 195 }
adam@328 196
adam@328 197 @inproceedings{IO,
adam@328 198 author = {Peyton Jones, Simon L. and Wadler, Philip},
adam@328 199 title = {Imperative functional programming},
adam@328 200 booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
adam@328 201 year = {1993},
adam@510 202 pages = {71--84}
adam@328 203 }
adam@328 204
adam@328 205 @InProceedings{separation,
adam@328 206 author = {John C. Reynolds},
adam@328 207 title = {Separation Logic: A Logic for Shared Mutable Data Structures},
adam@328 208 booktitle = {Proceedings of the IEEE Symposium on Logic in Computer Science},
adam@510 209 year = {2002},
adam@510 210 pages = {55--74}
adam@338 211 }
adam@338 212
adam@338 213 @article{Okasaki,
adam@338 214 author = {Okasaki, Chris},
adam@338 215 title = {Red-black trees in a functional setting},
adam@338 216 journal = {J. Funct. Program.},
adam@338 217 volume = {9},
adam@338 218 issue = {4},
adam@338 219 year = {1999},
adam@338 220 pages = {471--477},
adam@338 221 }
adam@342 222
adam@342 223 @Article{DeBruijn,
adam@342 224 author = "Nicolas G. de Bruijn",
adam@342 225 title = "Lambda-calculus notation with nameless dummies: a tool for automatic formal manipulation with application to the {Church-Rosser} theorem",
adam@342 226 journal = "Indag. Math.",
adam@342 227 volume = "34(5)",
adam@342 228 pages = "381--392",
adam@342 229 year = "1972"
adam@342 230 }
adam@343 231
adam@343 232 @INPROCEEDINGS{GirardsParadox,
adam@343 233 author = {Thierry Coquand},
adam@343 234 title = {An Analysis of {Girard's} Paradox},
adam@343 235 booktitle = {Proceedings of the Symposium on Logic in Computer Science},
adam@343 236 year = {1986},
adam@343 237 pages = {227--236}
adam@343 238 }
adam@344 239
adam@344 240 @inproceedings{PCC,
adam@344 241 author = {George C. Necula},
adam@344 242 title = {Proof-carrying code},
adam@344 243 booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
adam@344 244 year = {1997},
adam@510 245 pages = {106--119}
adam@344 246 }
adam@344 247
adam@344 248 @inproceedings{XCAP,
adam@344 249 author = {Ni, Zhaozhong and Shao, Zhong},
adam@344 250 title = {Certified assembly programming with embedded code pointers},
adam@344 251 booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
adam@344 252 year = {2006},
adam@510 253 pages = {320--333}
adam@344 254 }
adam@346 255
adam@346 256 @TechReport{IT,
adam@346 257 title = "A Tutorial on Recursive Types in {Coq}",
adam@346 258 author = "Eduardo Gim\'enez",
adam@346 259 year = "1998",
adam@346 260 month = may,
adam@346 261 number = "0221",
adam@346 262 institution = "INRIA",
adam@346 263 }
adam@347 264
adam@347 265 @inproceedings{BigStep,
adam@347 266 author = {Xavier Leroy and Herv\'e Grall},
adam@347 267 title = {Coinductive big-step operational semantics},
adam@347 268 year = {2006},
adam@510 269 booktitle = {Proceedings of the 15th European Symposium on Programming},
adam@510 270 pages = {54--68}
adam@347 271 }
adam@355 272
adam@355 273 @InBook{WinskelDomains,
adam@355 274 author = "Glynn Winskel",
adam@355 275 title = "The Formal Semantics of Programming Languages",
adam@355 276 year = "1993",
adam@355 277 publisher = "MIT Press",
adam@355 278 chapter = "8"
adam@355 279 }
adam@356 280
adam@356 281 @article{Capretta,
adam@356 282 author = {Venanzio Capretta},
adam@356 283 title = {General Recursion via Coinductive Types},
adam@356 284 journal = {Logical Methods in Computer Science},
adam@356 285 volume = 1,
adam@356 286 number = 2,
adam@356 287 year = 2005,
adam@356 288 pages = {1--18},
adam@356 289 }
adam@356 290
adam@356 291 @inproceedings{Megacz,
adam@356 292 author = {Adam Megacz},
adam@356 293 title = {A coinductive monad for prop-bounded recursion},
adam@356 294 booktitle = {Proceedings of the {ACM} Workshop Programming
adam@356 295 Languages meets Program Verification},
adam@356 296 pages = {11--20},
adam@356 297 year = {2007},
adam@356 298 }
adam@358 299
adam@358 300 @inproceedings{modules,
adam@358 301 author = {MacQueen, David},
adam@358 302 title = {Modules for {Standard ML}},
adam@358 303 booktitle = {Proceedings of the 1984 ACM Symposium on LISP and Functional Programming},
adam@358 304 year = {1984},
adam@358 305 pages = {198--207},
adam@358 306 }
adam@358 307
adam@358 308 @inproceedings{typeclasses,
adam@358 309 author = {Wadler, P. and Blott, S.},
adam@358 310 title = {How to make ad-hoc polymorphism less ad hoc},
adam@358 311 booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
adam@358 312 year = {1989},
adam@510 313 pages = {60--76}
adam@358 314 }
adam@360 315
adam@360 316 @inproceedings{reflection,
adam@360 317 author = {Boutin, Samuel},
adam@360 318 title = {Using reflection to build efficient and certified decision procedures},
adam@360 319 booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
adam@360 320 year = {1997},
adam@510 321 pages = {515--529}
adam@360 322 }
adam@364 323
adam@364 324 @inproceedings{JMeq,
adam@364 325 author = {McBride, Conor},
adam@364 326 title = {Elimination with a Motive},
adam@364 327 booktitle = {Proceedings of the International Workshop on Types for Proofs and Programs},
adam@364 328 year = {2000},
adam@364 329 pages = {197--216}
adam@364 330 }
adam@364 331
adam@364 332 @phdthesis{AxiomK,
adam@364 333 author = {Thomas Streicher},
adam@364 334 title = {Semantical Investigations into Intensional Type Theory},
adam@364 335 type = {Habilitationsschrift},
adam@364 336 school = {LMU M\"unchen},
adam@364 337 year= {1993}
adam@364 338 }
adam@381 339
adam@381 340 @article{BGB,
adam@381 341 author = {Geoffrey Washburn and Stephanie Weirich},
adam@381 342 title = {Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism},
adam@381 343 journal = {J. Funct. Program.},
adam@381 344 volume = {18},
adam@381 345 number = {1},
adam@381 346 year = {2008},
adam@381 347 pages = {87--140},
adam@381 348 publisher = {Cambridge University Press},
adam@381 349 address = {New York, NY, USA},
adam@381 350 }
adam@381 351
adam@381 352 @InProceedings{PhoasICFP08,
adam@381 353 author = {Adam Chlipala},
adam@381 354 title = {Parametric Higher-Order Abstract Syntax for Mechanized Semantics},
adam@381 355 booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming},
adam@381 356 year = {2008},
adam@381 357 pages = {143--156}
adam@381 358 }
adam@381 359
adam@381 360 @article{parametricity,
adam@381 361 author = {Reynolds, J.C.},
adam@381 362 year = {1983},
adam@381 363 title = {Types, abstraction, and parametric polymorphism},
adam@381 364 journal = {Information Processing},
adam@381 365 pages = {513--523}
adam@381 366 }
adam@381 367
adam@381 368 @InProceedings{CompilerPOPL10,
adam@381 369 author = {Adam Chlipala},
adam@381 370 title = {A Verified Compiler for an Impure Functional Language},
adam@381 371 booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
adam@381 372 year = {2010},
adam@510 373 pages = {93--106}
adam@381 374 }
adam@387 375
adam@387 376 @inproceedings{Isar,
adam@387 377 author = {Wenzel, Markus},
adam@387 378 title = {Isar - A Generic Interpretative Approach to Readable Formal Proof Documents},
adam@387 379 booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics},
adam@387 380 year = {1999},
adam@510 381 pages = {167--184}
adam@387 382 }
adam@394 383
adam@394 384 @article{continuations,
adam@394 385 author = {Reynolds, John C.},
adam@394 386 title = {The discoveries of continuations},
adam@394 387 journal = {Lisp Symb. Comput.},
adam@394 388 issue_date = {Nov. 1993},
adam@394 389 volume = {6},
adam@394 390 number = {3-4},
adam@394 391 month = nov,
adam@394 392 year = {1993},
adam@394 393 issn = {0892-4635},
adam@394 394 pages = {233--248},
adam@394 395 numpages = {16},
adam@394 396 url = {http://dx.doi.org/10.1007/BF01019459},
adam@394 397 doi = {10.1007/BF01019459},
adam@394 398 acmid = {198114},
adam@394 399 publisher = {Kluwer Academic Publishers},
adam@394 400 address = {Hingham, MA, USA},
adam@394 401 keywords = {continuation, continuation-passing style, semantics},
adam@394 402 }
adam@394 403
adam@394 404 @article{unification,
adam@394 405 author = {Robinson, J. A.},
adam@394 406 title = {A Machine-Oriented Logic Based on the Resolution Principle},
adam@394 407 journal = {J. ACM},
adam@394 408 issue_date = {Jan. 1965},
adam@394 409 volume = {12},
adam@394 410 number = {1},
adam@394 411 month = jan,
adam@394 412 year = {1965},
adam@394 413 issn = {0004-5411},
adam@394 414 pages = {23--41},
adam@394 415 numpages = {19},
adam@394 416 url = {http://doi.acm.org/10.1145/321250.321253},
adam@394 417 doi = {10.1145/321250.321253},
adam@394 418 acmid = {321253},
adam@394 419 publisher = {ACM},
adam@394 420 address = {New York, NY, USA},
adam@394 421 }
adam@395 422
adam@395 423 @ARTICLE{whyfp,
adam@395 424 author = {John Hughes},
adam@395 425 title = {Why Functional Programming Matters},
adam@395 426 journal = {The Computer Journal},
adam@395 427 year = {1984},
adam@395 428 volume = {32},
adam@395 429 pages = {98--107}
adam@395 430 }
adam@395 431
adam@395 432 @Book{Prolog,
adam@395 433 author = "Leon Sterling and Ehud Shapiro",
adam@395 434 title = "The Art of Prolog, 2nd Edition",
adam@395 435 year = "1994",
adam@395 436 publisher = "MIT Press"
adam@395 437 }
adam@395 438
adam@395 439 @Book{LogicProgramming,
adam@395 440 author = "John W. Lloyd",
adam@395 441 title = "Foundations of Logic Programming, 2nd Edition",
adam@395 442 year = "1987",
adam@395 443 publisher = "Springer"
adam@395 444 }
adam@395 445
adam@395 446 @InBook{deriving,
adam@395 447 title = "Haskell 98 Language and Libraries: The Revised Report",
adam@395 448 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 449 year = "1998",
adam@395 450 chapter = "4.3.3",
adam@395 451 url = {http://www.haskell.org/onlinereport/decls.html#derived-decls}
adam@395 452 }