cpdt.bib 13 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
@Book{TAPL,
  author       = "Benjamin C. Pierce",
  title        = "Types and Programming Languages",
  year         = "2002",
  publisher    = "MIT Press"
}

@Book{CAR,
  author       = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore",
  title        = "Computer-Aided Reasoning: An Approach",
  year         = "2000",
  publisher    = "Kluwer Academic Publishers"
}

@Article{AMD,
  author = {J Strother Moore and Tom Lynch and Matt Kaufmann},
  title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm},
  journal = {IEEE Transactions on Computers},
  volume = {47(9)},
20
  pages = {913--926},
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
  year = {1998}
}

@Book{Piton,
  author={J Strother Moore},
  title = {Piton: A Mechanically Verified Assembly-Level Language},
  year         = "1996",
  series       = "Automated Reasoning Series",
  publisher    = "Kluwer Academic Publishers"
}

@Article{Nqthm,
  title = {The {Boyer-Moore} Theorem Prover and Its Interactive Enhancement},
  author = {Robert S. Boyer and Matt Kaufmann and J Strother Moore},
  journal = {Computers and Mathematics with Applications},
  volume = {29(2)},
  year = {1995},
  pages = {27--62}
}

@Article{4C,
  author = {Gonthier, Georges},
  year = {2008},
  title = {Formal Proof--The Four-Color Theorem},
  journal = {Notices of the American Mathematical Society},
  volume = {55(11)},
47
  pages = {1382--1393}
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75
}

@Article{CompCert,
  author = {Leroy, Xavier},
  year = {2009},
  title = {A formally verified compiler back-end},
  journal = {Journal of Automated Reasoning},
  volume = {43(4)},
  pages = {363--446}
}

@InProceedings{seL4,
    author =  {Gerwin Klein 
    and Kevin Elphinstone 
    and Gernot Heiser
    and June Andronick 
    and David Cock
    and Philip Derrin
    and Dhammika Elkaduwe
    and Kai Engelhardt
    and Rafal Kolanski
    and Michael Norrish
    and Thomas Sewell
    and Harvey Tuch
    and Simon Winwood},
    title =        {{seL4}: Formal Verification of an {OS} Kernel},
    booktitle =    {Proceedings of the 22nd {ACM Symposium on Operating Systems Principles}},
    year =         {2009},
76
    pages =        {207--220}
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
}

@Book{Isabelle/HOL,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  volume	= 2283,
  year		= 2002
}

@Book{Isabelle,
  author = {Paulson, Lawrence C.},
  year = {1994},
  title = {Isabelle: A Generic Theorem Prover},
  series = {Lecture Notes in Computer Science},
  volume = {828},
  publisher = {Springer}
}

@Book{CoqArt,
  author       = "Bertot, Yves and Cast\'eran, Pierre",
  title        = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions",
  series       = "Texts in Theoretical Computer Science",
  year         = "2004",
  publisher    = "Springer Verlag",
}

@unpublished{CoqManual,
  author = "{Coq Development Team}",
107 108
  title = "The {Coq} proof assistant reference manual, version 8.4",
  year = 2012,
109 110
  url={http://coq.inria.fr/refman/}
}
111 112 113 114 115 116

@inproceedings{CIC,
  author = {Christine Paulin-Mohring},
  title = {Inductive Definitions in the System {Coq} - Rules and Properties},
  year = {1993},
  booktitle = {Proceedings of the International Conference on {Typed Lambda Calculi and Applications}},
117
  pages = {328--345}
118 119 120 121 122 123 124
}

@inproceedings{SetsInTypes,
  author    = {Benjamin Werner},
  title     = {Sets in Types, Types in Sets},
  booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
  year      = {1997},
125
  pages     = {530--546}
126 127 128 129 130 131 132 133 134
}

@article{CoC,
  author = {Thierry Coquand and G\'erard Huet},
  title = {The {Calculus} of {Constructions}},
  journal = {Information and Computation},
  volume = {76(2-3)},
  year = {1988}
}
135

136
@inproceedings{GADT,
137 138
  author = {Hongwei Xi and Chiyan Chen and Gang Chen},
  title = {Guarded Recursive Datatype Constructors},
139 140 141
  booktitle = {Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = {2003},
  pages = {224--235}
142
}
143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162

@article{Curry,
  title={Functionality in Combinatory Logic},
  author = {H. B. Curry},
  journal = {Proceedings of the National Academy of Sciences of the United States of America},
  volume = {20(11)},
  year = {1934},
  pages = {584--590}
}

@incollection{Howard,
  author = {Howard, William A.},
  title = {The formulae-as-types notion of construction},
  editor = {Seldin, Jonathan P. and Hindley, J. Roger},
  booktitle = {To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
  publisher = {Academic Press},
  pages = {479--490},
  year = {1980},
  note = {Original paper manuscript from 1969}
}
163 164 165 166 167 168

@inproceedings{HOAS,
 author = {Pfenning, F. and Elliot, C.},
 title = {Higher-order abstract syntax},
 booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation},
 year = {1988},
169
 pages = {199--208}
170
} 
171 172 173 174 175 176 177 178 179

@article{HOU,
 author = {G\'erard Huet},
 title = {The undecidability of unification in third order logic},
 journal = {Information and Control},
 voluem = {22(3)},
 year = {1973},
 pages = {257--267}
}
Adam Chlipala's avatar
Adam Chlipala committed
180 181 182 183 184 185 186 187 188 189 190 191 192 193

@InBook{TAPLNatDed,
  author       = "Benjamin C. Pierce",
  title        = "Types and Programming Languages",
  year         = "2002",
  publisher    = "MIT Press",
  chapter      = "9.4"
}

@inproceedings{Monads,
 author = {Wadler, Philip},
 title = {The essence of functional programming},
 booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {1992},
194
 pages = {1--14}
Adam Chlipala's avatar
Adam Chlipala committed
195 196 197 198 199 200 201
} 

@inproceedings{IO,
 author = {Peyton Jones, Simon L. and Wadler, Philip},
 title = {Imperative functional programming},
 booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {1993},
202
 pages = {71--84}
Adam Chlipala's avatar
Adam Chlipala committed
203 204 205 206 207 208
} 

@InProceedings{separation,
  author = 	 {John C. Reynolds},
  title = 	 {Separation Logic: A Logic for Shared Mutable Data Structures},
  booktitle =    {Proceedings of the IEEE Symposium on Logic in Computer Science},
209 210
  year = 	 {2002},
  pages =        {55--74}
Adam Chlipala's avatar
Adam Chlipala committed
211 212 213 214 215 216 217 218 219 220 221
}

@article{Okasaki,
 author = {Okasaki, Chris},
 title = {Red-black trees in a functional setting},
 journal = {J. Funct. Program.},
 volume = {9},
 issue = {4},
 year = {1999},
 pages = {471--477},
} 
Adam Chlipala's avatar
Adam Chlipala committed
222 223 224 225 226 227 228 229 230

@Article{DeBruijn,
  author =       "Nicolas G. de Bruijn",
  title =        "Lambda-calculus notation with nameless dummies: a tool for automatic formal manipulation with application to the {Church-Rosser} theorem",
  journal =      "Indag. Math.",
  volume =       "34(5)",
  pages =        "381--392",
  year =         "1972"
}
Adam Chlipala's avatar
Adam Chlipala committed
231 232 233 234 235 236 237 238

@INPROCEEDINGS{GirardsParadox,
    author = {Thierry Coquand},
    title = {An Analysis of {Girard's} Paradox},
    booktitle = {Proceedings of the Symposium on Logic in Computer Science},
    year = {1986},
    pages = {227--236}
}
239 240 241 242 243 244

@inproceedings{PCC,
 author = {George C. Necula},
 title = {Proof-carrying code},
 booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {1997},
245
 pages = {106--119}
246 247 248 249 250 251 252
}

@inproceedings{XCAP,
 author = {Ni, Zhaozhong and Shao, Zhong},
 title = {Certified assembly programming with embedded code pointers},
 booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {2006},
253
 pages = {320--333}
254
 }
255 256 257 258 259 260 261 262 263

@TechReport{IT,
  title =	 "A Tutorial on Recursive Types in {Coq}",
  author =	 "Eduardo Gim\'enez",
  year =	 "1998",
  month =	 may,
  number =	 "0221",
  institution =	 "INRIA",
}
264 265 266 267 268

@inproceedings{BigStep,
 author = {Xavier Leroy and Herv\'e Grall},
 title = {Coinductive big-step operational semantics},
 year = {2006},
269 270
 booktitle = {Proceedings of the 15th European Symposium on Programming},
 pages = {54--68}
271
}
272 273 274 275 276 277 278 279

@InBook{WinskelDomains,
  author       = "Glynn Winskel",
  title        = "The Formal Semantics of Programming Languages",
  year         = "1993",
  publisher    = "MIT Press",
  chapter      = "8"
}
280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298

@article{Capretta,
  author     = {Venanzio Capretta},
  title      = {General Recursion via Coinductive Types},
  journal    = {Logical Methods in Computer Science},
  volume     = 1,
  number     = 2,
  year       = 2005,
  pages      = {1--18},
}

@inproceedings{Megacz,
 author = {Adam Megacz},
 title = {A coinductive monad for prop-bounded recursion},
 booktitle =   {Proceedings of the {ACM} Workshop Programming
                Languages meets Program Verification},
 pages = {11--20},
 year = {2007},
}
Adam Chlipala's avatar
Adam Chlipala committed
299 300 301 302 303 304 305 306 307 308 309 310 311 312

@inproceedings{modules,
 author = {MacQueen, David},
 title = {Modules for {Standard ML}},
 booktitle = {Proceedings of the 1984 ACM Symposium on LISP and Functional Programming},
 year = {1984},
 pages = {198--207},
} 

@inproceedings{typeclasses,
 author = {Wadler, P. and Blott, S.},
 title = {How to make ad-hoc polymorphism less ad hoc},
 booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {1989},
313
 pages = {60--76}
Adam Chlipala's avatar
Adam Chlipala committed
314
} 
315 316 317 318 319 320

@inproceedings{reflection,
  author    = {Boutin, Samuel},
  title     = {Using reflection to build efficient and certified decision procedures},
  booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
  year      = {1997},
321
  pages     = {515--529}
322
}
323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338

@inproceedings{JMeq,
  author = {McBride, Conor},
  title = {Elimination with a Motive},
  booktitle = {Proceedings of the International Workshop on Types for Proofs and Programs},
  year = {2000},
  pages = {197--216}
}

@phdthesis{AxiomK,
  author = {Thomas Streicher},
  title = {Semantical Investigations into Intensional Type Theory},
  type = {Habilitationsschrift},
  school = {LMU M\"unchen},
  year= {1993}
}
Adam Chlipala's avatar
Adam Chlipala committed
339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372

@article{BGB,
 author = {Geoffrey Washburn and Stephanie Weirich},
 title = {Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism},
 journal = {J. Funct. Program.},
 volume = {18},
 number = {1},
 year = {2008},
 pages = {87--140},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@InProceedings{PhoasICFP08,
author = {Adam Chlipala},
title = {Parametric Higher-Order Abstract Syntax for Mechanized Semantics},
booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming},
year = {2008},
pages = {143--156}
}

@article{parametricity,
 author = {Reynolds, J.C.},
 year = {1983},
 title = {Types, abstraction, and parametric polymorphism},
 journal = {Information Processing},
 pages = {513--523}
}

@InProceedings{CompilerPOPL10,
author = {Adam Chlipala},
title = {A Verified Compiler for an Impure Functional Language},
booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
year = {2010},
373
pages = {93--106}
Adam Chlipala's avatar
Adam Chlipala committed
374
}
Adam Chlipala's avatar
Adam Chlipala committed
375 376 377 378 379 380

@inproceedings{Isar,
 author = {Wenzel, Markus},
 title = {Isar - A Generic Interpretative Approach to Readable Formal Proof Documents},
 booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics},
 year = {1999},
381
 pages = {167--184}
Adam Chlipala's avatar
Adam Chlipala committed
382
} 
383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421

@article{continuations,
 author = {Reynolds, John C.},
 title = {The discoveries of continuations},
 journal = {Lisp Symb. Comput.},
 issue_date = {Nov. 1993},
 volume = {6},
 number = {3-4},
 month = nov,
 year = {1993},
 issn = {0892-4635},
 pages = {233--248},
 numpages = {16},
 url = {http://dx.doi.org/10.1007/BF01019459},
 doi = {10.1007/BF01019459},
 acmid = {198114},
 publisher = {Kluwer Academic Publishers},
 address = {Hingham, MA, USA},
 keywords = {continuation, continuation-passing style, semantics},
}

@article{unification,
 author = {Robinson, J. A.},
 title = {A Machine-Oriented Logic Based on the Resolution Principle},
 journal = {J. ACM},
 issue_date = {Jan. 1965},
 volume = {12},
 number = {1},
 month = jan,
 year = {1965},
 issn = {0004-5411},
 pages = {23--41},
 numpages = {19},
 url = {http://doi.acm.org/10.1145/321250.321253},
 doi = {10.1145/321250.321253},
 acmid = {321253},
 publisher = {ACM},
 address = {New York, NY, USA},
}
422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452

@ARTICLE{whyfp,
    author = {John Hughes},
    title = {Why Functional Programming Matters},
    journal = {The Computer Journal},
    year = {1984},
    volume = {32},
    pages = {98--107}
}

@Book{Prolog,
  author       = "Leon Sterling and Ehud Shapiro",
  title        = "The Art of Prolog, 2nd Edition",
  year         = "1994",
  publisher    = "MIT Press"
}

@Book{LogicProgramming,
  author       = "John W. Lloyd",
  title        = "Foundations of Logic Programming, 2nd Edition",
  year         = "1987",
  publisher    = "Springer"
}

@InBook{deriving,
  title =	 "Haskell 98 Language and Libraries: The Revised Report",
  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",
  year =	 "1998",
  chapter =      "4.3.3",
  url =          {http://www.haskell.org/onlinereport/decls.html#derived-decls}
}