1% BibTeX database for the Isabelle documentation 2 3%publishers 4@string{AP="Academic Press"} 5@string{CUP="Cambridge University Press"} 6@string{IEEE="IEEE Computer Society Press"} 7@string{LNCS="Lecture Notes in Computer Science"} 8@string{MIT="MIT Press"} 9@string{NH="North-Holland"} 10@string{Prentice="Prentice-Hall"} 11@string{PH="Prentice-Hall"} 12@string{Springer="Springer-Verlag"} 13 14%institutions 15@string{CUCL="Computer Laboratory, University of Cambridge"} 16@string{Edinburgh="Department of Computer Science, University of Edinburgh"} 17@string{TUM="Department of Informatics, Technical University of Munich"} 18 19%journals 20@string{AI="Artificial Intelligence"} 21@string{FAC="Formal Aspects of Computing"} 22@string{JAR="Journal of Automated Reasoning"} 23@string{JCS="Journal of Computer Security"} 24@string{JFP="Journal of Functional Programming"} 25@string{JLC="Journal of Logic and Computation"} 26@string{JLP="Journal of Logic Programming"} 27@string{JSC="Journal of Symbolic Computation"} 28@string{JSL="Journal of Symbolic Logic"} 29@string{PROYAL="Proceedings of the Royal Society of London"} 30@string{SIGPLAN="{SIGPLAN} Notices"} 31@string{TISSEC="ACM Transactions on Information and System Security"} 32 33%conferences 34@string{CADE="International Conference on Automated Deduction"} 35@string{POPL="Symposium on Principles of Programming Languages"} 36@string{TYPES="Types for Proofs and Programs"} 37 38 39%A 40 41@incollection{abramsky90, 42 author = {Samson Abramsky}, 43 title = {The Lazy Lambda Calculus}, 44 pages = {65-116}, 45 editor = {David A. Turner}, 46 booktitle = {Research Topics in Functional Programming}, 47 publisher = {Addison-Wesley}, 48 year = 1990} 49 50@Unpublished{abrial93, 51 author = {J. R. Abrial and G. Laffitte}, 52 title = {Towards the Mechanization of the Proofs of Some Classical 53 Theorems of Set Theory}, 54 note = {preprint}, 55 year = 1993, 56 month = Feb} 57 58@incollection{aczel77, 59 author = {Peter Aczel}, 60 title = {An Introduction to Inductive Definitions}, 61 pages = {739-782}, 62 crossref = {barwise-handbk}} 63 64@Book{aczel88, 65 author = {Peter Aczel}, 66 title = {Non-Well-Founded Sets}, 67 publisher = {CSLI}, 68 year = 1988} 69 70@inproceedings{Aehlig-Haftmann-Nipkow:2008:nbe, 71 author = {Klaus Aehlig and Florian Haftmann and Tobias Nipkow}, 72 title = {A Compiled Implementation of Normalization by Evaluation}, 73 booktitle = {TPHOLs '08: Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics}, 74 year = {2008}, 75 isbn = {978-3-540-71065-3}, 76 pages = {352--367}, 77 publisher = Springer, 78 series = LNCS, 79 volume = {5170}, 80 editor = {Otmane A\"{\i}t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar} 81} 82 83@InProceedings{alf, 84 author = {Lena Magnusson and Bengt {Nordstr\"{o}m}}, 85 title = {The {ALF} Proof Editor and Its Proof Engine}, 86 crossref = {types93}, 87 pages = {213-237}} 88 89@inproceedings{andersson-1993, 90 author = "Arne Andersson", 91 title = "Balanced Search Trees Made Simple", 92 editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides", 93 booktitle = "WADS 1993", 94 series = LNCS, 95 volume = {709}, 96 pages = "61--70", 97 year = 1993, 98 publisher = Springer} 99 100@book{andrews86, 101 author = "Peter Andrews", 102 title = "An Introduction to Mathematical Logic and Type Theory: to Truth 103through Proof", 104 publisher = AP, 105 series = "Computer Science and Applied Mathematics", 106 year = 1986} 107 108@InProceedings{Aspinall:2000:eProof, 109 author = {David Aspinall}, 110 title = {Protocols for Interactive {e-Proof}}, 111 booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)}, 112 year = 2000, 113 note = {Unpublished work-in-progress paper, 114 \url{http://homepages.inf.ed.ac.uk/da/papers/drafts/eproof.ps.gz}} 115} 116 117@InProceedings{Aspinall:TACAS:2000, 118 author = {David Aspinall}, 119 title = {{P}roof {G}eneral: A Generic Tool for Proof Development}, 120 booktitle = {Tools and Algorithms for the Construction and Analysis of 121 Systems (TACAS)}, 122 year = 2000, 123 publisher = Springer, 124 series = LNCS, 125 volume = 1785, 126 pages = "38--42" 127} 128 129@Misc{isamode, 130 author = {David Aspinall}, 131 title = {Isamode --- {U}sing {I}sabelle with {E}macs}, 132 note = {\url{http://homepages.inf.ed.ac.uk/da/Isamode/}} 133} 134 135@Misc{proofgeneral, 136 author = {David Aspinall}, 137 title = {{P}roof {G}eneral}, 138 note = {\url{http://proofgeneral.inf.ed.ac.uk/}} 139} 140 141%B 142 143@inproceedings{backes-brown-2010, 144 title = "Analytic Tableaux for Higher-Order Logic with Choice", 145 author = "Julian Backes and Chad E. Brown", 146 booktitle={Automated Reasoning: IJCAR 2010}, 147 editor={J. Giesl and R. H\"ahnle}, 148 publisher = Springer, 149 series = LNCS, 150 volume = 6173, 151 pages = "76--90", 152 year = 2010} 153 154@book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow}, 155title="Term Rewriting and All That",publisher=CUP,year=1998} 156 157@manual{isabelle-locale, 158 author = {Clemens Ballarin}, 159 title = {Tutorial to Locales and Locale Interpretation}, 160 institution = TUM, 161 note = {\url{https://isabelle.in.tum.de/doc/locales.pdf}} 162} 163 164@article{Ballarin2014, 165 author = {Ballarin, Clemens}, 166 journal = JAR, 167 publisher = Springer, 168 title = {Locales: A Module System for Mathematical Theories}, 169 volume = 52, 170 number = 2, 171 pages = {123--153}, 172 url = {https://doi.org/10.1007/s10817-013-9284-7}, 173 year = {2014}} 174 175@InCollection{Barendregt-Geuvers:2001, 176 author = {H. Barendregt and H. Geuvers}, 177 title = {Proof Assistants using Dependent Type Systems}, 178 booktitle = {Handbook of Automated Reasoning}, 179 publisher = {Elsevier}, 180 year = 2001, 181 editor = {A. Robinson and A. Voronkov} 182} 183 184@inproceedings{cvc3, 185 author = {Clark Barrett and Cesare Tinelli}, 186 title = {{CVC3}}, 187 booktitle = {CAV}, 188 editor = {Werner Damm and Holger Hermanns}, 189 volume = {4590}, 190 series = LNCS, 191 pages = {298--302}, 192 publisher = {Springer}, 193 year = {2007} 194} 195 196@inproceedings{cvc4, 197 author = {Clark Barrett and 198 Christopher L. Conway and 199 Morgan Deters and 200 Liana Hadarean and 201 Dejan Jovanovic and 202 Tim King and 203 Andrew Reynolds and 204 Cesare Tinelli}, 205 title = {{CVC4}}, 206 booktitle = {CAV 2011}, 207 pages = {171--177}, 208 editor = {Ganesh Gopalakrishnan and 209 Shaz Qadeer}, 210 publisher = {Springer}, 211 series = LNCS, 212 volume = {6806}, 213 year = {2011} 214} 215 216@incollection{basin91, 217 author = {David Basin and Matt Kaufmann}, 218 title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental 219 Comparison}, 220 crossref = {huet-plotkin91}, 221 pages = {89-119}} 222 223@Unpublished{HOL-Library, 224 author = {Gertrud Bauer and Tobias Nipkow and Oheimb, David von and 225 Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and 226 Markus Wenzel}, 227 title = {The Supplemental {Isabelle/HOL} Library}, 228 note = {Part of the Isabelle distribution, 229 \url{https://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, 230 year = 2002 231} 232 233@InProceedings{Bauer-Wenzel:2000:HB, 234 author = {Gertrud Bauer and Markus Wenzel}, 235 title = {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in 236 {I}sabelle/{I}sar}, 237 booktitle = {Types for Proofs and Programs: TYPES'99}, 238 editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m 239 and Jan Smith}, 240 series = {LNCS}, 241 year = 2000 242} 243 244@InProceedings{Bauer-Wenzel:2001, 245 author = {Gertrud Bauer and Markus Wenzel}, 246 title = {Calculational reasoning revisited --- an {Isabelle/Isar} experience}, 247 crossref = {tphols2001}} 248 249@inproceedings{leo2, 250 author = "Christoph Benzm{\"u}ller and Lawrence C. Paulson and Frank Theiss and Arnaud Fietzke", 251 title = "{LEO-II}---A Cooperative Automatic Theorem Prover for Higher-Order Logic", 252 editor = "Alessandro Armando and Peter Baumgartner and Gilles Dowek", 253 booktitle = "Automated Reasoning: IJCAR 2008", 254 publisher = Springer, 255 series = LNCS, 256 volume = 5195, 257 pages = "162--170", 258 year = 2008} 259 260@inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL, 261 author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian}, 262 booktitle = {Theorem Proving in Higher Order Logics}, 263 pages = {131--146}, 264 title = {Turning Inductive into Equational Specifications}, 265 year = {2009} 266} 267 268@INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL, 269 crossref = "tphols2000", 270 title = "Proof terms for simply typed higher order logic", 271 author = "Stefan Berghofer and Tobias Nipkow", 272 pages = "38--52"} 273 274@inproceedings{berghofer-nipkow-2004, 275 author = {Stefan Berghofer and Tobias Nipkow}, 276 title = {Random Testing in {I}sabelle/{HOL}}, 277 pages = {230--239}, 278 editor = "J. Cuellar and Z. Liu", 279 booktitle = {{SEFM} 2004}, 280 publisher = IEEE, 281 year = 2004} 282 283@InProceedings{Berghofer-Nipkow:2002, 284 author = {Stefan Berghofer and Tobias Nipkow}, 285 title = {Executing Higher Order Logic}, 286 booktitle = {Types for Proofs and Programs: TYPES'2000}, 287 editor = {P. Callaghan and Z. Luo and J. McKinna and R. Pollack}, 288 series = LNCS, 289 publisher = Springer, 290 volume = 2277, 291 year = 2002} 292 293@InProceedings{Berghofer-Wenzel:1999:TPHOL, 294 author = {Stefan Berghofer and Markus Wenzel}, 295 title = {Inductive datatypes in {HOL} --- lessons learned in 296 {F}ormal-{L}ogic {E}ngineering}, 297 crossref = {tphols99}} 298 299 300@InProceedings{Bezem-Coquand:2005, 301 author = {M.A. Bezem and T. Coquand}, 302 title = {Automating {Coherent Logic}}, 303 booktitle = {LPAR-12}, 304 year = 2005, 305 editor = {G. Sutcliffe and A. Voronkov}, 306 volume = 3835, 307 series = LNCS, 308 publisher = Springer} 309 310@manual{isabelle-datatypes, 311 author = {Julian Biendarra and Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel}, 312 title = {Defining (Co)datatypes and Primitively (Co)recursive Functions in {Isabelle\slash HOL}}, 313 institution = {TU Munich}, 314 note = {\url{https://isabelle.in.tum.de/doc/datatypes.pdf}}} 315 316@book{Bird-Wadler,author="Richard Bird and Philip Wadler", 317title="Introduction to Functional Programming",publisher=PH,year=1988} 318 319@book{Bird-Haskell,author="Richard Bird", 320title="Introduction to Functional Programming using Haskell", 321publisher=PH,year=1998} 322 323@manual{isabelle-nitpick, 324 author = {Jasmin Christian Blanchette}, 325 title = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle\slash {HOL}}, 326 institution = TUM, 327 note = {\url{https://isabelle.in.tum.de/doc/nitpick.pdf}} 328} 329 330@manual{isabelle-sledgehammer, 331 author = {Jasmin Christian Blanchette}, 332 title = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle\slash {HOL}}, 333 institution = TUM, 334 note = {\url{https://isabelle.in.tum.de/doc/sledgehammer.pdf}} 335} 336 337@manual{isabelle-corec, 338 author = {Jasmin Christian Blanchette and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel}, 339 title = {Defining Nonprimitively Corecursive Functions in {Isabelle\slash HOL}}, 340 institution = {TU Munich}, 341 note = {\url{https://isabelle.in.tum.de/doc/corec.pdf}}} 342 343@inproceedings{blanchette-nipkow-2010, 344 title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder", 345 author = "Jasmin Christian Blanchette and Tobias Nipkow", 346 crossref = {itp2010}} 347 348@inproceedings{blanchette-et-al-2015-wit, 349 author = {Jasmin Christian Blanchette and 350 Andrei Popescu and 351 Dmitriy Traytel}, 352 title = {Witnessing (Co)datatypes}, 353 booktitle = {24th European Symposium on Programming, {ESOP} 2015}, 354 pages = {359--382}, 355 year = {2015}, 356 editor = {Jan Vitek}, 357 series = {LNCS}, 358 volume = {9032}, 359 publisher = {Springer} 360} 361 362@inproceedings{blanchette-et-al-2015-fouco, 363 author = {Jasmin Christian Blanchette and 364 Andrei Popescu and 365 Dmitriy Traytel}, 366 title = {Foundational extensible corecursion: A proof assistant perspective}, 367 booktitle = {20th {ACM} {SIGPLAN} International Conference on 368 Functional Programming, {ICFP} 2015}, 369 pages = {192--204}, 370 year = {2015}, 371 editor = {Kathleen Fisher and 372 John H. Reppy}, 373 publisher = {{ACM}}, 374} 375 376@misc{blanchette-et-al-201x-amico, 377 author = {Jasmin Christian Blanchette and 378 Aymeric Bouzy and 379 Andreas Lochbihler and 380 Andrei Popescu and 381 Dmitriy Traytel}, 382 title = {Friends with benefits: Implementing corecursion in foundational proof assistants}, 383 howpublished = "\url{http://www21.in.tum.de/~blanchet/amico.pdf}", 384 year = 2016} 385 386@inproceedings{blanchette-et-al-2014-impl, 387 author = "Jasmin Christian Blanchette and Johannes H{\"o}lzl 388 and Andreas Lochbihler and Lorenz Panny and Andrei Popescu and Dmitriy Traytel", 389 title = "Truly Modular (Co)datatypes for {I}sabelle/{HOL}", 390 year = 2014, 391 publisher = "Springer", 392 editor = "Gerwin Klein and Ruben Gamboa", 393 booktitle = {5th International Conference on Interactive Theorem Proving, ITP 2014}, 394 series = LNCS, 395 volume = 8558, 396 pages = "93--110" 397} 398 399@inproceedings{why3, 400 author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich}, 401 title = {{Why3}: Shepherd Your Herd of Provers}, 402 editor = "K. Rustan M. Leino and Micha\l{} Moskal", 403 booktitle = {Boogie 2011}, 404 pages = "53--64", 405 year = 2011 406} 407 408@inproceedings{alt-ergo, 409 author = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean and St\'ephane Lescuyer}, 410 title = {Implementing Polymorphism in {SMT} Solvers}, 411 booktitle = {SMT '08}, 412 pages = "1--5", 413 publisher = "ACM", 414 series = "ICPS", 415 year = 2008, 416 editor = {Clark Barrett and Leonardo de Moura}} 417% /BPR 418% and Domagoj Babic and Amit Goel 419 420@inproceedings{boehme-nipkow-2010, 421 author={Sascha B\"ohme and Tobias Nipkow}, 422 title={Sledgehammer: Judgement Day}, 423 booktitle={Automated Reasoning: IJCAR 2010}, 424 editor={J. Giesl and R. H\"ahnle}, 425 publisher=Springer, 426 series=LNCS, 427 volume = 6173, 428 pages = "107--121", 429 year=2010} 430 431@inproceedings{bouton-et-al-2009, 432 author = {Thomas Bouton and 433 Diego Caminha B. de Oliveira and 434 David D{\'{e}}harbe and 435 Pascal Fontaine}, 436 title = {{veriT}: An Open, Trustable and Efficient {SMT}-Solver}, 437 year = {2009}, 438 pages = {151--156}, 439 editor = {Renate A. Schmidt}, 440 booktitle = {Automated Deduction --- CADE-22}, 441 series = {Lecture Notes in Computer Science}, 442 volume = {5663}, 443 publisher = {Springer} 444} 445 446@Article{boyer86, 447 author = {Robert Boyer and Ewing Lusk and William McCune and Ross 448 Overbeek and Mark Stickel and Lawrence Wos}, 449 title = {Set Theory in First-Order Logic: Clauses for {G\"{o}del's} 450 Axioms}, 451 journal = JAR, 452 year = 1986, 453 volume = 2, 454 number = 3, 455 pages = {287-327}} 456 457@book{bm79, 458 author = {Robert S. Boyer and J Strother Moore}, 459 title = {A Computational Logic}, 460 publisher = {Academic Press}, 461 year = 1979} 462 463@book{bm88book, 464 author = {Robert S. Boyer and J Strother Moore}, 465 title = {A Computational Logic Handbook}, 466 publisher = {Academic Press}, 467 year = 1988} 468 469@inproceedings{satallax, 470 author = "Chad E. Brown", 471 title = "Reducing Higher-Order Theorem Proving to a Sequence of {SAT} Problems", 472 booktitle = {Automated Deduction --- CADE-23}, 473 publisher = Springer, 474 series = LNCS, 475 volume = 6803, 476 pages = "147--161", 477 editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans", 478 year = 2011} 479 480@Article{debruijn72, 481 author = {N. G. de Bruijn}, 482 title = {Lambda Calculus Notation with Nameless Dummies, 483 a Tool for Automatic Formula Manipulation, 484 with Application to the {Church-Rosser Theorem}}, 485 journal = {Indag. Math.}, 486 volume = 34, 487 pages = {381-392}, 488 year = 1972} 489 490@InProceedings{bulwahnKN07, 491 author = {Lukas Bulwahn and Alexander Krauss and Tobias Nipkow}, 492 title = {Finding Lexicographic Orders for Termination Proofs in {Isabelle/HOL}}, 493 crossref = {tphols2007}, 494 pages = {38--53} 495} 496 497@InProceedings{bulwahn-et-al:2008:imperative, 498 author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erk��k and John Matthews}, 499 title = {Imperative Functional Programming with {Isabelle/HOL}}, 500 crossref = {tphols2008}, 501} 502% pages = {38--53} 503 504@Article{ban89, 505 author = {M. Burrows and M. Abadi and R. M. Needham}, 506 title = {A Logic of Authentication}, 507 journal = PROYAL, 508 year = 1989, 509 volume = 426, 510 pages = {233-271}} 511 512%C 513 514@PhdThesis{Chaieb-thesis, 515 author = {Amine Chaieb}, 516 title = {Automated methods for formal proofs in simple arithmetics and algebra}, 517 school = {Technische Universit\"at M\"unchen}, 518 year = 2008, 519 note = {\url{http://www4.in.tum.de/~chaieb/pubs/pdf/diss.pdf}}} 520 521@InProceedings{Chaieb-Wenzel:2007, 522 author = {Amine Chaieb and Makarius Wenzel}, 523 title = {Context aware Calculation and Deduction --- 524 Ring Equalities via {Gr\"obner Bases} in {Isabelle}}, 525 booktitle = {Towards Mechanized Mathematical Assistants (CALCULEMUS 2007)}, 526 editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger}, 527 series = "LNAI", 528 volume = 4573, 529 year = 2007, 530 publisher = Springer 531} 532 533@TechReport{camilleri92, 534 author = {J. Camilleri and T. F. Melham}, 535 title = {Reasoning with Inductively Defined Relations in the 536 {HOL} Theorem Prover}, 537 institution = CUCL, 538 year = 1992, 539 number = 265, 540 month = Aug} 541 542@Book{charniak80, 543 author = {E. Charniak and C. K. Riesbeck and D. V. McDermott}, 544 title = {Artificial Intelligence Programming}, 545 publisher = {Lawrence Erlbaum Associates}, 546 year = 1980} 547 548@article{church40, 549 author = "Alonzo Church", 550 title = "A Formulation of the Simple Theory of Types", 551 journal = JSL, 552 year = 1940, 553 volume = 5, 554 pages = "56-68"} 555 556@book{ClarkeGP-book,author="Edmund Clarke and Orna Grumberg and Doron Peled", 557title="Model Checking",publisher=MIT,year=1999} 558 559@PhdThesis{coen92, 560 author = {Martin D. Coen}, 561 title = {Interactive Program Derivation}, 562 school = {University of Cambridge}, 563 note = {Computer Laboratory Technical Report 272}, 564 month = nov, 565 year = 1992} 566 567@book{constable86, 568 author = {R. L. Constable and others}, 569 title = {Implementing Mathematics with the Nuprl Proof 570 Development System}, 571 publisher = Prentice, 572 year = 1986} 573 574@inproceedings{cruanes-2014, 575 author = "Simon Cruanes", 576 title = "Logtk: A {Logic ToolKit} for Automated Reasoning, and its Implementation", 577 booktitle = {4th Workshop on Practical Aspects of Automated Reasoning, PAAR@IJCAR 578 2014, Vienna, Austria, 2014}, 579 year = 2014, 580 note = {Presented at the Practical Aspects of Automated Reasoning (PAAR) workshop}} 581 582%D 583 584@Book{davey-priestley, 585 author = {B. A. Davey and H. A. Priestley}, 586 title = {Introduction to Lattices and Order}, 587 publisher = CUP, 588 year = 1990} 589 590@Book{devlin79, 591 author = {Keith J. Devlin}, 592 title = {Fundamentals of Contemporary Set Theory}, 593 publisher = {Springer}, 594 year = 1979} 595 596@inproceedings{di-gianantonio-miculan-2003, 597 author = {Di Gianantonio, Pietro and 598 Marino Miculan}, 599 title = {A Unifying Approach to Recursive and Co-recursive Definitions}, 600 booktitle = {TYPES 2002}, 601 year = {2003}, 602 pages = {148--161}, 603 editor = {Herman Geuvers and 604 Freek Wiedijk}, 605 publisher = {Springer}, 606 series = {LNCS}, 607 volume = {2646} 608} 609 610@book{dummett, 611 author = {Michael Dummett}, 612 title = {Elements of Intuitionism}, 613 year = 1977, 614 publisher = {Oxford University Press}} 615 616@misc{yices, 617 author = {Bruno Dutertre and Leonardo de Moura}, 618 title = {The {Yices} {SMT} Solver}, 619 howpublished = "\url{http://yices.csl.sri.com/tool-paper.pdf}", 620 year = 2006} 621 622@incollection{dybjer91, 623 author = {Peter Dybjer}, 624 title = {Inductive Sets and Families in {Martin-L{\"o}f's} Type 625 Theory and Their Set-Theoretic Semantics}, 626 crossref = {huet-plotkin91}, 627 pages = {280-306}} 628 629@Article{dyckhoff, 630 author = {Roy Dyckhoff}, 631 title = {Contraction-Free Sequent Calculi for Intuitionistic Logic}, 632 journal = JSL, 633 year = 1992, 634 volume = 57, 635 number = 3, 636 pages = {795-807}} 637 638%F 639 640@Article{IMPS, 641 author = {William M. Farmer and Joshua D. Guttman and F. Javier 642 Thayer}, 643 title = {{IMPS}: An Interactive Mathematical Proof System}, 644 journal = JAR, 645 volume = 11, 646 number = 2, 647 year = 1993, 648 pages = {213-248}} 649 650@article{Farmer:2008, 651 author = {William M. Farmer}, 652 title = {The seven virtues of simple type theory}, 653 journal = {J. Applied Logic}, 654 volume = {6}, 655 number = {3}, 656 pages = {267--286}, 657 year = {2008}, 658 url = {https://doi.org/10.1016/j.jal.2007.11.001}, 659} 660 661@InProceedings{felty91a, 662 Author = {Amy Felty}, 663 Title = {A Logic Program for Transforming Sequent Proofs to Natural 664 Deduction Proofs}, 665 crossref = {extensions91}, 666 pages = {157-178}} 667 668@Article{fleuriot-jcm, 669 author = {Jacques Fleuriot and Lawrence C. Paulson}, 670 title = {Mechanizing Nonstandard Real Analysis}, 671 journal = {LMS Journal of Computation and Mathematics}, 672 year = 2000, 673 volume = 3, 674 pages = {140-190}, 675 note = {\url{http://www.lms.ac.uk/jcm/3/lms1999-027/}} 676} 677 678@TechReport{frost93, 679 author = {Jacob Frost}, 680 title = {A Case Study of Co-induction in {Isabelle HOL}}, 681 institution = CUCL, 682 number = 308, 683 year = 1993, 684 month = Aug} 685 686%revised version of frost93 687@TechReport{frost95, 688 author = {Jacob Frost}, 689 title = {A Case Study of Co-induction in {Isabelle}}, 690 institution = CUCL, 691 number = 359, 692 year = 1995, 693 month = Feb} 694 695@inproceedings{OBJ, 696 author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud 697 and J. Meseguer}, 698 title = {Principles of {OBJ2}}, 699 booktitle = POPL, 700 year = 1985, 701 pages = {52-66}} 702 703%G 704 705@book{gallier86, 706 author = {J. H. Gallier}, 707 title = {Logic for Computer Science: 708 Foundations of Automatic Theorem Proving}, 709 year = 1986, 710 publisher = {Harper \& Row}} 711 712@Book{galton90, 713 author = {Antony Galton}, 714 title = {Logic for Information Technology}, 715 publisher = {Wiley}, 716 year = 1990} 717 718@Article{Gentzen:1935, 719 author = {G. Gentzen}, 720 title = {Untersuchungen {\"u}ber das logische {S}chlie{\ss}en}, 721 journal = {Math. Zeitschrift}, 722 year = 1935 723} 724 725@InProceedings{gimenez-codifying, 726 author = {Eduardo Gim{\'e}nez}, 727 title = {Codifying Guarded Definitions with Recursive Schemes}, 728 crossref = {types94}, 729 pages = {39-59} 730} 731 732@book{girard89, 733 author = {Jean-Yves Girard}, 734 title = {Proofs and Types}, 735 year = 1989, 736 publisher = CUP, 737 note = {Translated by Yves Lafont and Paul Taylor}} 738 739@TechReport{Gordon:1985:HOL, 740 author = {M. J. C. Gordon}, 741 title = {{HOL}: A machine oriented formulation of higher order logic}, 742 institution = {University of Cambridge Computer Laboratory}, 743 year = 1985, 744 number = 68 745} 746 747@Book{mgordon-hol, 748 editor = {M. J. C. Gordon and T. F. Melham}, 749 title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}, 750 publisher = CUP, 751 year = 1993} 752 753@book{mgordon79, 754 author = {Michael J. C. Gordon and Robin Milner and Christopher P. 755 Wadsworth}, 756 title = {Edinburgh {LCF}: A Mechanised Logic of Computation}, 757 year = 1979, 758 publisher = {Springer}, 759 series = LNCS, 760 volume = 78} 761 762@inproceedings{Gunter-HOL92,author={Elsa L. Gunter}, 763title={Why we can't have {SML} style datatype declarations in {HOL}}, 764booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.\ 765IFIP TC10/WG10.2 Intl. Workshop, 1992}, 766editor={L.J.M. Claesen and M.J.C. Gordon}, 767publisher=NH,year=1993,pages={561--568}} 768 769@InProceedings{gunter-trees, 770 author = {Elsa L. Gunter}, 771 title = {A Broader Class of Trees for Recursive Type Definitions for 772 {HOL}}, 773 crossref = {hug93}, 774 pages = {141-154}} 775 776%H 777 778@inproceedings{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement, 779 author = {Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow}, 780 title = {Data Refinement in {Isabelle/HOL}}, 781 booktitle = {Interactive Theorem Proving (ITP 2013)}, 782 pages = {100-115}, 783 year = 2013, 784 publisher = Springer, 785 series = {Lecture Notes in Computer Science}, 786 volume = {7998}, 787 editor = {S. Blazy and C. Paulin-Mohring and D. Pichardie} 788} 789 790@inproceedings{Haftmann-Nipkow:2010:code, 791 author = {Florian Haftmann and Tobias Nipkow}, 792 title = {Code Generation via Higher-Order Rewrite Systems}, 793 booktitle = {Functional and Logic Programming: 10th International Symposium: FLOPS 2010}, 794 year = 2010, 795 publisher = Springer, 796 series = LNCS, 797 editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal}, 798 volume = 6009 799} 800 801@InProceedings{Haftmann-Wenzel:2006:classes, 802 author = {Florian Haftmann and Makarius Wenzel}, 803 title = {Constructive Type Classes in {Isabelle}}, 804 editor = {T. Altenkirch and C. McBride}, 805 booktitle = {Types for Proofs and Programs, TYPES 2006}, 806 publisher = {Springer}, 807 series = {LNCS}, 808 volume = {4502}, 809 year = {2007} 810} 811 812@InProceedings{Haftmann-Wenzel:2009, 813 author = {Florian Haftmann and Makarius Wenzel}, 814 title = {Local theory specifications in {Isabelle/Isar}}, 815 editor = {Stefano Berardi and Ferruccio Damiani and de Liguoro, Ugo}, 816 booktitle = {Types for Proofs and Programs, TYPES 2008}, 817 publisher = {Springer}, 818 series = {LNCS}, 819 volume = {5497}, 820 year = {2009} 821} 822 823@inproceedings{hindleymilner, 824 author = {L. Damas and H. Milner}, 825 title = {Principal type schemes for functional programs}, 826 booktitle = {ACM Symp. Principles of Programming Languages}, 827 year = 1982 828} 829 830@manual{isabelle-classes, 831 author = {Florian Haftmann}, 832 title = {Haskell-style type classes with {Isabelle}/{Isar}}, 833 institution = TUM, 834 note = {\url{https://isabelle.in.tum.de/doc/classes.pdf}} 835} 836 837@manual{isabelle-codegen, 838 author = {Florian Haftmann}, 839 title = {Code generation from Isabelle theories}, 840 institution = TUM, 841 note = {\url{https://isabelle.in.tum.de/doc/codegen.pdf}} 842} 843 844@Book{halmos60, 845 author = {Paul R. Halmos}, 846 title = {Naive Set Theory}, 847 publisher = {Van Nostrand}, 848 year = 1960} 849 850@book{HarelKT-DL,author={David Harel and Dexter Kozen and Jerzy Tiuryn}, 851title={Dynamic Logic},publisher=MIT,year=2000} 852 853@Book{hennessy90, 854 author = {Matthew Hennessy}, 855 title = {The Semantics of Programming Languages: An Elementary 856 Introduction Using Structural Operational Semantics}, 857 publisher = {Wiley}, 858 year = 1990} 859 860@article{waldmeister, 861 author = {Thomas Hillenbrand and Arnim Buch and Rolan Vogt and Bernd L\"ochner}, 862 title = "Waldmeister: High-Performance Equational Deduction", 863 journal = JAR, 864 volume = 18, 865 number = 2, 866 pages = {265--270}, 867 year = 1997} 868 869@article{hinze10, 870 author = {Hinze, Ralf}, 871 title = {Concrete stream calculus---{A}n extended study}, 872 journal = {J. Funct. Program.}, 873 volume = {20}, 874 issue = {Special Issue 5-6}, 875 year = {2010}, 876 issn = {1469-7653}, 877 pages = {463--535} 878} 879 880@inproceedings{sine, 881 author = "Kry\v{s}tof Hoder and Andrei Voronkov", 882 title = "Sine Qua Non for Large Theory Reasoning", 883 booktitle = {Automated Deduction --- CADE-23}, 884 publisher = Springer, 885 series = LNCS, 886 volume = 6803, 887 pages = "299--314", 888 editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans", 889 year = 2011} 890 891@book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman}, 892title={Introduction to Automata Theory, Languages, and Computation.}, 893publisher={Addison-Wesley},year=1979} 894 895@Article{haskell-report, 896 author = {Paul Hudak and Simon Peyton Jones and Philip Wadler}, 897 title = {Report on the Programming Language {Haskell}: A 898 Non-strict, Purely Functional Language}, 899 journal = SIGPLAN, 900 year = 1992, 901 volume = 27, 902 number = 5, 903 month = May, 904 note = {Version 1.2}} 905 906@Article{haskell-tutorial, 907 author = {Paul Hudak and Joseph H. Fasel}, 908 title = {A Gentle Introduction to {Haskell}}, 909 journal = SIGPLAN, 910 year = 1992, 911 volume = 27, 912 number = 5, 913 month = May} 914 915@inproceedings{Hoelzl-Huffman-Immler:2013:typeclasses, 916 author = {Johannes H{\"o}lzl and Fabian Immler and Brian Huffman}, 917 title = {Type Classes and Filters for Mathematical Analysis in {Isabelle/HOL}}, 918 booktitle = {Interactive Theorem Proving (ITP 2013)}, 919 editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David}, 920 year = 2013, 921 volume = 7998, 922 series = LNCS, 923 publisher = Springer, 924 isbn = {978-3-642-39633-5}, 925 pages = {279--294}} 926 927@book{Hudak-Haskell,author={Paul Hudak}, 928title={The Haskell School of Expression},publisher=CUP,year=2000} 929 930@article{huet75, 931 author = {G. P. Huet}, 932 title = {A Unification Algorithm for Typed $\lambda$-Calculus}, 933 journal = TCS, 934 volume = 1, 935 year = 1975, 936 pages = {27-57}} 937 938@article{huet78, 939 author = {G. P. Huet and B. Lang}, 940 title = {Proving and Applying Program Transformations Expressed with 941 Second-Order Patterns}, 942 journal = acta, 943 volume = 11, 944 year = 1978, 945 pages = {31-55}} 946 947@inproceedings{huet88, 948 author = {G{\'e}rard Huet}, 949 title = {Induction Principles Formalized in the {Calculus of 950 Constructions}}, 951 booktitle = {Programming of Future Generation Computers}, 952 editor = {K. Fuchi and M. Nivat}, 953 year = 1988, 954 pages = {205-216}, 955 publisher = {Elsevier}} 956 957@inproceedings{Huffman-Kuncar:2013:lifting_transfer, 958 author = {Brian Huffman and Ond\v{r}ej Kun\v{c}ar}, 959 title = {{Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL}}, 960 booktitle = {Certified Programs and Proofs (CPP 2013)}, 961 year = 2013, 962 publisher = Springer, 963 series = {Lecture Notes in Computer Science}, 964 volume = {8307}, 965} 966 967@Book{Huth-Ryan-book, 968 author = {Michael Huth and Mark Ryan}, 969 title = {Logic in Computer Science. Modelling and reasoning about systems}, 970 publisher = CUP, 971 year = 2000} 972 973@InProceedings{Harrison:1996:MizarHOL, 974 author = {J. Harrison}, 975 title = {A {Mizar} Mode for {HOL}}, 976 pages = {203--220}, 977 crossref = {tphols96}} 978 979@misc{metis, 980 author = "Joe Hurd", 981 title = "Metis Theorem Prover", 982 note = "\url{http://www.gilith.com/software/metis/}"} 983 984%J 985 986@article{haskell-revised-report, 987 author = {Simon {Peyton Jones} and others}, 988 title = {The {Haskell} 98 Language and Libraries: The Revised Report}, 989 journal = {Journal of Functional Programming}, 990 volume = 13, 991 number = 1, 992 pages = {0--255}, 993 month = {Jan}, 994 year = 2003, 995 note = {\url{http://www.haskell.org/definition/}}} 996 997@book{jackson-2006, 998 author = "Daniel Jackson", 999 title = "Software Abstractions: Logic, Language, and Analysis", 1000 publisher = MIT, 1001 year = 2006} 1002 1003%K 1004 1005@InProceedings{kammueller-locales, 1006 author = {Florian Kamm{\"u}ller and Markus Wenzel and 1007 Lawrence C. Paulson}, 1008 title = {Locales: A Sectioning Concept for {Isabelle}}, 1009 crossref = {tphols99}} 1010 1011@book{Knuth3-75, 1012 author={Donald E. Knuth}, 1013 title={The Art of Computer Programming, Volume 3: Sorting and Searching}, 1014 publisher={Addison-Wesley}, 1015 year=1975} 1016 1017@Article{korf85, 1018 author = {R. E. Korf}, 1019 title = {Depth-First Iterative-Deepening: an Optimal Admissible 1020 Tree Search}, 1021 journal = AI, 1022 year = 1985, 1023 volume = 27, 1024 pages = {97-109}} 1025 1026@inproceedings{korovin-2009, 1027 title = "Instantiation-Based Automated Reasoning: From Theory to Practice", 1028 author = "Konstantin Korovin", 1029 editor = "Renate A. Schmidt", 1030 booktitle = {Automated Deduction --- CADE-22}, 1031 series = "LNAI", 1032 volume = {5663}, 1033 pages = "163--166", 1034 year = 2009, 1035 publisher = "Springer"} 1036 1037@inproceedings{korovin-sticksel-2010, 1038 author = {Konstantin Korovin and 1039 Christoph Sticksel}, 1040 title = {{iP}rover-{E}q: An Instantiation-Based Theorem Prover with Equality}, 1041 pages = {196--202}, 1042 booktitle={Automated Reasoning: IJCAR 2010}, 1043 editor={J. Giesl and R. H\"ahnle}, 1044 publisher = Springer, 1045 series = LNCS, 1046 volume = 6173, 1047 year = 2010} 1048 1049@InProceedings{krauss2006, 1050 author = {Alexander Krauss}, 1051 title = {Partial Recursive Functions in {Higher-Order Logic}}, 1052 crossref = {ijcar2006}, 1053 pages = {589--603}} 1054 1055@PhdThesis{krauss_phd, 1056 author = {Alexander Krauss}, 1057 title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic}, 1058 school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}, 1059 year = {2009}, 1060 address = {Germany} 1061} 1062 1063@manual{isabelle-function, 1064 author = {Alexander Krauss}, 1065 title = {Defining Recursive Functions in {Isabelle/HOL}}, 1066 institution = TUM, 1067 note = {\url{https://isabelle.in.tum.de/doc/functions.pdf}} 1068} 1069 1070@inproceedings{Kuncar:2015, 1071 author = {Ondrej Kuncar}, 1072 title = {Correctness of {Isabelle's} Cyclicity Checker: Implementability of Overloading 1073 in Proof Assistants}, 1074 booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs, 1075 {CPP} 2015, Mumbai, India, January 15-17, 2015}, 1076 year = {2015}, 1077 url = {http://doi.acm.org/10.1145/2676724.2693175}, 1078 doi = {10.1145/2676724.2693175}, 1079} 1080 1081@inproceedings{Kuncar-Popescu:2015, 1082 author = {Ondrej Kuncar and Andrei Popescu}, 1083 title = {A Consistent Foundation for {Isabelle/HOL}}, 1084 editor = {Christian Urban and Xingyuan Zhang}, 1085 booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP} 1086 2015, Nanjing, China, August 24-27, 2015, Proceedings}, 1087 year = {2015}, 1088 url = {https://doi.org/10.1007/978-3-319-22102-1_16}, 1089 series = {Lecture Notes in Computer Science}, 1090 volume = {9236}, 1091 publisher = {Springer}, 1092} 1093 1094@Book{kunen80, 1095 author = {Kenneth Kunen}, 1096 title = {Set Theory: An Introduction to Independence Proofs}, 1097 publisher = NH, 1098 year = 1980} 1099 1100%L 1101 1102@manual{OCaml, 1103 author = {Xavier Leroy and others}, 1104 title = {The Objective Caml system -- Documentation and user's manual}, 1105 note = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}} 1106 1107@misc{agsyHOL, 1108 author = "Fredrik Lindblad", 1109 title = "{agsyHOL}", 1110 note = "\url{https://github.com/frelindb/agsyHOL}"} 1111 1112@incollection{lochbihler-2010, 1113 title = "Coinductive", 1114 author = "Andreas Lochbihler", 1115 booktitle = "The Archive of Formal Proofs", 1116 editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson", 1117 publisher = "\url{https://isa-afp.org/entries/Coinductive.shtml}", 1118 month = "Feb.", 1119 year = 2010} 1120 1121@inproceedings{lochbihler-hoelzl-2014, 1122 author = {Andreas Lochbihler and 1123 Johannes H{\"{o}}lzl}, 1124 title = {Recursive Functions on Lazy Lists via Domains and Topologies}, 1125 booktitle = {Interactive Theorem Proving --- 5th International Conference, {ITP} 1126 2014}, 1127 pages = {341--357}, 1128 year = {2014}, 1129 editor = {Gerwin Klein and 1130 Ruben Gamboa}, 1131 series = LNCS, 1132 volume = {8558}, 1133 publisher = {Springer}, 1134} 1135 1136@book{loveland-78, 1137 author = "D. W. Loveland", 1138 title = "Automated Theorem Proving: A Logical Basis", 1139 year = 1978, 1140 publisher = "North-Holland Publishing Co."} 1141 1142@InProceedings{lowe-fdr, 1143 author = {Gavin Lowe}, 1144 title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key 1145 Protocol using {CSP} and {FDR}}, 1146 booktitle = {Tools and Algorithms for the Construction and Analysis 1147 of Systems: second international workshop, TACAS '96}, 1148 editor = {T. Margaria and B. Steffen}, 1149 series = {LNCS 1055}, 1150 year = 1996, 1151 publisher = {Springer}, 1152 pages = {147-166}} 1153 1154%M 1155 1156@Article{mw81, 1157 author = {Zohar Manna and Richard Waldinger}, 1158 title = {Deductive Synthesis of the Unification Algorithm}, 1159 journal = SCP, 1160 year = 1981, 1161 volume = 1, 1162 number = 1, 1163 pages = {5-48}} 1164 1165@InProceedings{martin-nipkow, 1166 author = {Ursula Martin and Tobias Nipkow}, 1167 title = {Ordered Rewriting and Confluence}, 1168 crossref = {cade10}, 1169 pages = {366-380}} 1170 1171@book{martinlof84, 1172 author = {Per Martin-L{\"o}f}, 1173 title = {Intuitionistic type theory}, 1174 year = 1984, 1175 publisher = {Bibliopolis}} 1176 1177@inproceedings{Matichuk-et-al:2014, 1178 author = {Daniel Matichuk and Makarius Wenzel and Toby C. Murray}, 1179 title = {An {Isabelle} Proof Method Language}, 1180 editor = {Gerwin Klein and Ruben Gamboa}, 1181 booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP} 1182 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, 1183 Austria}, 1184 year = {2014}, 1185 url = {https://doi.org/10.1007/978-3-319-08970-6_25}, 1186 doi = {10.1007/978-3-319-08970-6_25}, 1187 series = "LNCS", 1188 volume = {8558}, 1189 publisher = {Springer}, 1190} 1191 1192@incollection{melham89, 1193 author = {Thomas F. Melham}, 1194 title = {Automating Recursive Type Definitions in Higher Order 1195 Logic}, 1196 pages = {341-386}, 1197 crossref = {birtwistle89}} 1198 1199@Article{Miller:1991, 1200 author = {Dale Miller}, 1201 title = {A Logic Programming Language with Lambda-Abstraction, Function Variables, 1202 and Simple Unification}, 1203 journal = {Journal of Logic and Computation}, 1204 year = 1991, 1205 volume = 1, 1206 number = 4 1207} 1208 1209@Article{miller-mixed, 1210 Author = {Dale Miller}, 1211 Title = {Unification Under a Mixed Prefix}, 1212 journal = JSC, 1213 volume = 14, 1214 number = 4, 1215 pages = {321-358}, 1216 Year = 1992} 1217 1218@Article{milner78, 1219 author = {Robin Milner}, 1220 title = {A Theory of Type Polymorphism in Programming}, 1221 journal = "J. Comp.\ Sys.\ Sci.", 1222 year = 1978, 1223 volume = 17, 1224 pages = {348-375}} 1225 1226@TechReport{milner-ind, 1227 author = {Robin Milner}, 1228 title = {How to Derive Inductions in {LCF}}, 1229 institution = Edinburgh, 1230 year = 1980, 1231 type = {note}} 1232 1233@Article{milner-coind, 1234 author = {Robin Milner and Mads Tofte}, 1235 title = {Co-induction in Relational Semantics}, 1236 journal = TCS, 1237 year = 1991, 1238 volume = 87, 1239 pages = {209-220}} 1240 1241@Book{milner89, 1242 author = {Robin Milner}, 1243 title = {Communication and Concurrency}, 1244 publisher = Prentice, 1245 year = 1989} 1246 1247@book{SML,author="Robin Milner and Mads Tofte and Robert Harper", 1248title="The Definition of Standard ML",publisher=MIT,year=1990} 1249 1250@PhdThesis{monahan84, 1251 author = {Brian Q. Monahan}, 1252 title = {Data Type Proofs using Edinburgh {LCF}}, 1253 school = {University of Edinburgh}, 1254 year = 1984} 1255 1256@article{MuellerNvOS99, 1257author= 1258{Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch}, 1259title={{HOLCF = HOL + LCF}},journal=JFP,year=1999,volume=9,pages={191--223}} 1260 1261@Manual{Muzalewski:Mizar, 1262 title = {An Outline of {PC} {Mizar}}, 1263 author = {Micha{\l} Muzalewski}, 1264 organization = {Fondation of Logic, Mathematics and Informatics 1265 --- Mizar Users Group}, 1266 year = 1993, 1267 note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}} 1268} 1269 1270%N 1271 1272@InProceedings{NaraschewskiW-TPHOLs98, 1273 author = {Wolfgang Naraschewski and Markus Wenzel}, 1274 title = 1275{Object-Oriented Verification based on Record Subtyping in 1276 Higher-Order Logic}, 1277 crossref = {tphols98}} 1278 1279@inproceedings{nazareth-nipkow, 1280 author = {Dieter Nazareth and Tobias Nipkow}, 1281 title = {Formal Verification of Algorithm {W}: The Monomorphic Case}, 1282 crossref = {tphols96}, 1283 pages = {331-345}, 1284 year = 1996} 1285 1286@Article{needham-schroeder, 1287 author = "Roger M. Needham and Michael D. Schroeder", 1288 title = "Using Encryption for Authentication in Large Networks 1289 of Computers", 1290 journal = cacm, 1291 volume = 21, 1292 number = 12, 1293 pages = "993-999", 1294 month = dec, 1295 year = 1978} 1296 1297@inproceedings{nipkow-W, 1298 author = {Wolfgang Naraschewski and Tobias Nipkow}, 1299 title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}}, 1300 booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96}, 1301 editor = {E. Gim{\'e}nez and C. Paulin-Mohring}, 1302 publisher = Springer, 1303 series = LNCS, 1304 volume = 1512, 1305 pages = {317-332}, 1306 year = 1998} 1307 1308@InCollection{nipkow-sorts93, 1309 author = {T. Nipkow}, 1310 title = {Order-Sorted Polymorphism in {Isabelle}}, 1311 booktitle = {Logical Environments}, 1312 publisher = CUP, 1313 year = 1993, 1314 editor = {G. Huet and G. Plotkin}, 1315 pages = {164--188} 1316} 1317 1318@Misc{nipkow-types93, 1319 author = {Tobias Nipkow}, 1320 title = {Axiomatic Type Classes (in {I}sabelle)}, 1321 howpublished = {Presentation at the workshop \emph{Types for Proof and Programs}, Nijmegen}, 1322 year = 1993 1323} 1324 1325@inproceedings{Nipkow-CR, 1326 author = {Tobias Nipkow}, 1327 title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})}, 1328 booktitle = {Automated Deduction --- CADE-13}, 1329 editor = {M. McRobbie and J.K. Slaney}, 1330 publisher = Springer, 1331 series = LNCS, 1332 volume = 1104, 1333 pages = {733-747}, 1334 year = 1996} 1335 1336% WAS Nipkow-LICS-93 1337@InProceedings{nipkow-patterns, 1338 title = {Functional Unification of Higher-Order Patterns}, 1339 author = {Tobias Nipkow}, 1340 pages = {64-74}, 1341 crossref = {lics8}, 1342 url = {\url{ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html}}, 1343 keywords = {unification}} 1344 1345@article{nipkow-IMP, 1346 author = {Tobias Nipkow}, 1347 title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, 1348 journal = FAC, 1349 volume = 10, 1350 pages = {171-186}, 1351 year = 1998} 1352 1353@inproceedings{Nipkow-TYPES02, 1354 author = {Tobias Nipkow}, 1355 title = {{Structured Proofs in Isar/HOL}}, 1356 booktitle = {Types for Proofs and Programs (TYPES 2002)}, 1357 editor = {H. Geuvers and F. Wiedijk}, 1358 year = 2003, 1359 publisher = Springer, 1360 series = LNCS, 1361 volume = 2646, 1362 pages = {259-278}} 1363 1364@manual{isabelle-HOL, 1365 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, 1366 title = {{Isabelle}'s Logics: {HOL}}, 1367 institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t 1368 M{\"u}nchen and Computer Laboratory, University of Cambridge}, 1369 note = {\url{https://isabelle.in.tum.de/doc/logics-HOL.pdf}}} 1370 1371@article{nipkow-prehofer, 1372 author = {Tobias Nipkow and Christian Prehofer}, 1373 title = {Type Reconstruction for Type Classes}, 1374 journal = JFP, 1375 volume = 5, 1376 number = 2, 1377 year = 1995, 1378 pages = {201-224}} 1379 1380@InProceedings{Nipkow-Prehofer:1993, 1381 author = {T. Nipkow and C. Prehofer}, 1382 title = {Type checking type classes}, 1383 booktitle = {ACM Symp.\ Principles of Programming Languages}, 1384 year = 1993 1385} 1386 1387@Book{isa-tutorial, 1388 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, 1389 title = {Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic}, 1390 publisher = Springer, 1391 year = 2002, 1392 series = LNCS, 1393 volume = 2283} 1394 1395@Article{noel, 1396 author = {Philippe No{\"e}l}, 1397 title = {Experimenting with {Isabelle} in {ZF} Set Theory}, 1398 journal = JAR, 1399 volume = 10, 1400 number = 1, 1401 pages = {15-58}, 1402 year = 1993} 1403 1404@book{nordstrom90, 1405 author = {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith}, 1406 title = {Programming in {Martin-L{\"o}f}'s Type Theory. An 1407 Introduction}, 1408 publisher = {Oxford University Press}, 1409 year = 1990} 1410 1411%O 1412 1413@TechReport{scala-overview-tech-report, 1414 author = {Martin Odersky et al.}, 1415 title = {An Overview of the Scala Programming Language}, 1416 institution = {EPFL Lausanne, Switzerland}, 1417 year = 2004, 1418 number = {IC/2004/64} 1419} 1420 1421@Article{Oppen:1980, 1422 author = {D. C. Oppen}, 1423 title = {Pretty Printing}, 1424 journal = {ACM Transactions on Programming Languages and Systems}, 1425 year = 1980, 1426 volume = 2, 1427 number = 4} 1428 1429@Manual{pvs-language, 1430 title = {The {PVS} specification language}, 1431 author = {S. Owre and N. Shankar and J. M. Rushby}, 1432 organization = {Computer Science Laboratory, SRI International}, 1433 address = {Menlo Park, CA}, 1434 note = {Beta release}, 1435 year = 1993, 1436 month = apr, 1437 url = {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}} 1438 1439%P 1440 1441@inproceedings{panny-et-al-2014, 1442 author = "Lorenz Panny and Jasmin Christian Blanchette and Dmitriy Traytel", 1443 title = "Primitively (co)recursive definitions for {I}sabelle/{HOL}", 1444 year = 2014, 1445 booktitle = "Isabelle Workshop 2014" 1446} 1447 1448% replaces paulin92 1449@InProceedings{paulin-tlca, 1450 author = {Christine Paulin-Mohring}, 1451 title = {Inductive Definitions in the System {Coq}: Rules and 1452 Properties}, 1453 crossref = {tlca93}, 1454 pages = {328-345}} 1455 1456@Article{paulson:1983, 1457 author = {L. C. Paulson}, 1458 title = {A higher-order implementation of rewriting}, 1459 journal = {Science of Computer Programming}, 1460 year = 1983, 1461 volume = 3, 1462 pages = {119--149}, 1463 note = {\url{http://www.cl.cam.ac.uk/~lp15/papers/Reports/TR035-lcp-rewriting.pdf}}} 1464 1465@InProceedings{paulson-CADE, 1466 author = {Lawrence C. Paulson}, 1467 title = {A Fixedpoint Approach to Implementing (Co)Inductive 1468 Definitions}, 1469 pages = {148-161}, 1470 crossref = {cade12}} 1471 1472@InProceedings{paulson-COLOG, 1473 author = {Lawrence C. Paulson}, 1474 title = {A Formulation of the Simple Theory of Types (for 1475 {Isabelle})}, 1476 pages = {246-274}, 1477 crossref = {colog88}, 1478 url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}} 1479 1480@Article{paulson-coind, 1481 author = {Lawrence C. Paulson}, 1482 title = {Mechanizing Coinduction and Corecursion in Higher-Order 1483 Logic}, 1484 journal = JLC, 1485 year = 1997, 1486 volume = 7, 1487 number = 2, 1488 month = mar, 1489 pages = {175-204}} 1490 1491@article{paulson-numerical, 1492 author = {Lawrence C. Paulson}, 1493 title = {Organizing numerical theories using axiomatic type 1494 classes}, 1495 journal = JAR, 1496 year = 2004, 1497 volume = 33, 1498 number = 1, 1499 pages = {29-49}} 1500 1501@manual{isabelle-intro, 1502 author = {Lawrence C. Paulson}, 1503 title = {Old Introduction to {Isabelle}}, 1504 institution = CUCL, 1505 note = {\url{https://isabelle.in.tum.de/doc/intro.pdf}}} 1506 1507@manual{isabelle-logics, 1508 author = {Lawrence C. Paulson}, 1509 title = {{Isabelle's} Logics}, 1510 institution = CUCL, 1511 note = {\url{https://isabelle.in.tum.de/doc/logics.pdf}}} 1512 1513@manual{isabelle-ref, 1514 author = {Lawrence C. Paulson}, 1515 title = {The Old {Isabelle} Reference Manual}, 1516 institution = CUCL, 1517 note = {\url{https://isabelle.in.tum.de/doc/ref.pdf}}} 1518 1519@manual{isabelle-ZF, 1520 author = {Lawrence C. Paulson}, 1521 title = {{Isabelle}'s Logics: {FOL} and {ZF}}, 1522 institution = CUCL, 1523 note = {\url{https://isabelle.in.tum.de/doc/logics-ZF.pdf}}} 1524 1525@article{paulson-found, 1526 author = {Lawrence C. Paulson}, 1527 title = {The Foundation of a Generic Theorem Prover}, 1528 journal = JAR, 1529 volume = 5, 1530 number = 3, 1531 pages = {363-397}, 1532 year = 1989, 1533 url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}} 1534 1535%replaces paulson-final 1536@Article{paulson-mscs, 1537 author = {Lawrence C. Paulson}, 1538 title = {Final Coalgebras as Greatest Fixed Points 1539 in {ZF} Set Theory}, 1540 journal = {Mathematical Structures in Computer Science}, 1541 year = 1999, 1542 volume = 9, 1543 number = 5, 1544 pages = {545-567}} 1545 1546@InCollection{paulson-generic, 1547 author = {Lawrence C. Paulson}, 1548 title = {Generic Automatic Proof Tools}, 1549 crossref = {wos-fest}, 1550 chapter = 3} 1551 1552@Article{paulson-gr, 1553 author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski}, 1554 title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of 1555 Choice}, 1556 journal = JAR, 1557 year = 1996, 1558 volume = 17, 1559 number = 3, 1560 month = dec, 1561 pages = {291-323}} 1562 1563@InCollection{paulson-fixedpt-milner, 1564 author = {Lawrence C. Paulson}, 1565 title = {A Fixedpoint Approach to (Co)inductive and 1566 (Co)datatype Definitions}, 1567 pages = {187-211}, 1568 crossref = {milner-fest}} 1569 1570@book{milner-fest, 1571 title = {Proof, Language, and Interaction: 1572 Essays in Honor of {Robin Milner}}, 1573 booktitle = {Proof, Language, and Interaction: 1574 Essays in Honor of {Robin Milner}}, 1575 publisher = MIT, 1576 year = 2000, 1577 editor = {Gordon Plotkin and Colin Stirling and Mads Tofte}} 1578 1579@InCollection{paulson-handbook, 1580 author = {Lawrence C. Paulson}, 1581 title = {Designing a Theorem Prover}, 1582 crossref = {handbk-lics2}, 1583 pages = {415-475}} 1584 1585@Book{paulson-isa-book, 1586 author = {Lawrence C. Paulson}, 1587 title = {Isabelle: A Generic Theorem Prover}, 1588 publisher = {Springer}, 1589 year = 1994, 1590 note = {LNCS 828}} 1591 1592@Book{isabelle-hol-book, 1593 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, 1594 title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, 1595 publisher = {Springer}, 1596 year = 2002, 1597 note = {LNCS 2283}} 1598 1599@InCollection{paulson-markt, 1600 author = {Lawrence C. Paulson}, 1601 title = {Tool Support for Logics of Programs}, 1602 booktitle = {Mathematical Methods in Program Development: 1603 Summer School Marktoberdorf 1996}, 1604 publisher = {Springer}, 1605 pages = {461-498}, 1606 year = {Published 1997}, 1607 editor = {Manfred Broy}, 1608 series = {NATO ASI Series F}} 1609 1610%replaces Paulson-ML and paulson91 1611@book{paulson-ml2, 1612 author = {Lawrence C. Paulson}, 1613 title = {{ML} for the Working Programmer}, 1614 year = 1996, 1615 edition = {2nd}, 1616 publisher = CUP, 1617 note = {\url{https://www.cl.cam.ac.uk/~lp15/MLbook}}} 1618 1619@article{paulson-natural, 1620 author = {Lawrence C. Paulson}, 1621 title = {Natural Deduction as Higher-order Resolution}, 1622 journal = JLP, 1623 volume = 3, 1624 pages = {237-258}, 1625 year = 1986, 1626 url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}} 1627 1628@Article{paulson-set-I, 1629 author = {Lawrence C. Paulson}, 1630 title = {Set Theory for Verification: {I}. {From} 1631 Foundations to Functions}, 1632 journal = JAR, 1633 volume = 11, 1634 number = 3, 1635 pages = {353-389}, 1636 year = 1993, 1637 url = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Sets/set-I.pdf}}} 1638 1639@Article{paulson-set-II, 1640 author = {Lawrence C. Paulson}, 1641 title = {Set Theory for Verification: {II}. {Induction} and 1642 Recursion}, 1643 journal = JAR, 1644 volume = 15, 1645 number = 2, 1646 pages = {167-215}, 1647 year = 1995, 1648 url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}} 1649 1650@article{paulson85, 1651 author = {Lawrence C. Paulson}, 1652 title = {Verifying the Unification Algorithm in {LCF}}, 1653 journal = SCP, 1654 volume = 5, 1655 pages = {143-170}, 1656 year = 1985} 1657 1658%replaces Paulson-LCF 1659@book{paulson87, 1660 author = {Lawrence C. Paulson}, 1661 title = {Logic and Computation: Interactive proof with Cambridge 1662 LCF}, 1663 year = 1987, 1664 publisher = CUP} 1665 1666@incollection{paulson700, 1667 author = {Lawrence C. Paulson}, 1668 title = {{Isabelle}: The Next 700 Theorem Provers}, 1669 crossref = {odifreddi90}, 1670 pages = {361-386}, 1671 url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}} 1672 1673% replaces paulson-ns and paulson-security 1674@Article{paulson-jcs, 1675 author = {Lawrence C. Paulson}, 1676 title = {The Inductive Approach to Verifying Cryptographic Protocols}, 1677 journal = JCS, 1678 year = 1998, 1679 volume = 6, 1680 pages = {85-128}} 1681 1682@Article{paulson-tls, 1683 author = {Lawrence C. Paulson}, 1684 title = {Inductive Analysis of the {Internet} Protocol {TLS}}, 1685 journal = TISSEC, 1686 month = aug, 1687 year = 1999, 1688 volume = 2, 1689 number = 3, 1690 pages = {332-351}} 1691 1692@Article{paulson-yahalom, 1693 author = {Lawrence C. Paulson}, 1694 title = {Relations Between Secrets: 1695 Two Formal Analyses of the {Yahalom} Protocol}, 1696 journal = JCS, 1697 volume = 9, 1698 number = 3, 1699 pages = {197-216}, 1700 year = 2001}} 1701 1702@article{pelletier86, 1703 author = {F. J. Pelletier}, 1704 title = {Seventy-five Problems for Testing Automatic Theorem 1705 Provers}, 1706 journal = JAR, 1707 volume = 2, 1708 pages = {191-216}, 1709 year = 1986, 1710 note = {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}} 1711 1712@InCollection{pitts93, 1713 author = {A. Pitts}, 1714 title = {The {HOL} Logic}, 1715 editor = {M. J. C. Gordon and T. F. Melham}, 1716 booktitle = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}, 1717 pages = {191--232}, 1718 publisher = CUP, 1719 year = 1993} 1720 1721@Article{pitts94, 1722 author = {Andrew M. Pitts}, 1723 title = {A Co-induction Principle for Recursively Defined Domains}, 1724 journal = TCS, 1725 volume = 124, 1726 pages = {195-219}, 1727 year = 1994} 1728 1729@Article{plaisted90, 1730 author = {David A. Plaisted}, 1731 title = {A Sequent-Style Model Elimination Strategy and a Positive 1732 Refinement}, 1733 journal = JAR, 1734 year = 1990, 1735 volume = 6, 1736 number = 4, 1737 pages = {389-402}} 1738 1739%Q 1740 1741@Article{quaife92, 1742 author = {Art Quaife}, 1743 title = {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set 1744 Theory}, 1745 journal = JAR, 1746 year = 1992, 1747 volume = 8, 1748 number = 1, 1749 pages = {91-147}} 1750 1751%R 1752 1753@TechReport{rasmussen95, 1754 author = {Ole Rasmussen}, 1755 title = {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting 1756 Experiment}, 1757 institution = {Computer Laboratory, University of Cambridge}, 1758 year = 1995, 1759 number = 364, 1760 month = may, 1761 url = {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}} 1762 1763@Book{reeves90, 1764 author = {Steve Reeves and Michael Clarke}, 1765 title = {Logic for Computer Science}, 1766 publisher = {Addison-Wesley}, 1767 year = 1990} 1768 1769@article{riazanov-voronkov-2002, 1770 author = "Alexander Riazanov and Andrei Voronkov", 1771 title = "The Design and Implementation of {Vampire}", 1772 journal = "Journal of AI Communications", 1773 year = 2002, 1774 volume = 15, 1775 number ="2/3", 1776 pages = "91--110"} 1777 1778@book{Rosen-DMA,author={Kenneth H. Rosen}, 1779title={Discrete Mathematics and Its Applications}, 1780publisher={McGraw-Hill},year=1998} 1781 1782@InProceedings{Rudnicki:1992:MizarOverview, 1783 author = {P. Rudnicki}, 1784 title = {An Overview of the {MIZAR} Project}, 1785 booktitle = {1992 Workshop on Types for Proofs and Programs}, 1786 year = 1992, 1787 organization = {Chalmers University of Technology}, 1788 publisher = {Bastad} 1789} 1790 1791@article{rutten05, 1792 author = {Jan J. M. M. Rutten}, 1793 title = {A coinductive calculus of streams}, 1794 journal = {Math. Struct. Comp. Sci.}, 1795 volume = 15, 1796 number = 1, 1797 year = 2005, 1798 pages = {93--147}, 1799} 1800 1801%S 1802 1803@inproceedings{saaltink-fme, 1804 author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and 1805 Dan Craigen and Irwin Meisels}, 1806 title = {An {EVES} Data Abstraction Example}, 1807 pages = {578-596}, 1808 crossref = {fme93}} 1809 1810@Article{Schroeder-Heister:1984, 1811 author = {Peter Schroeder-Heister}, 1812 title = {A Natural Extension of Natural Deduction}, 1813 journal = {Journal of Symbolic Logic}, 1814 year = 1984, 1815 volume = 49, 1816 number = 4 1817} 1818 1819@article{schulz-2002, 1820 author = "Stephan Schulz", 1821 title = "E---A Brainiac Theorem Prover", 1822 journal = "Journal of AI Communications", 1823 year = 2002, 1824 volume = 15, 1825 number ="2/3", 1826 pages = "111--126"} 1827 1828@inproceedings{slind-tfl, 1829 author = {Konrad Slind}, 1830 title = {Function Definition in Higher Order Logic}, 1831 crossref = {tphols96}, 1832 pages = {381-397}} 1833 1834@inproceedings{leo3, 1835 Author = {Alexander Steen and Max Wisniewski and Christoph 1836 Benzm{\"u}ller}, 1837 Booktitle = {Mathematical Software -- ICMS 2016}, 1838 Editor = {G.-M. Greuel and T. Koch and P. Paule and 1839 A. Sommese}, 1840 Publisher = {Springer}, 1841 Series = {LNCS}, 1842 Title = {Agent-Based {HOL} Reasoning}, 1843 Volume = 9725, 1844 Year = 2016, 1845 Pages = {75-81} 1846} 1847 1848@incollection{sternagel-thiemann-2015, 1849 title = "Deriving Class Instances for Datatypes", 1850 author = "Christian Sternagel and Ren\'e Thiemann", 1851 booktitle = "The Archive of Formal Proofs", 1852 editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson", 1853 publisher = "\url{https://isa-afp.org/entries/Deriving.shtml}", 1854 month = "March", 1855 year = 2015} 1856 1857@inproceedings{snark, 1858 author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood}, 1859 title = {Deductive composition of astronomical software from subroutine libraries}, 1860 pages = "341--355", 1861 crossref = {cade12}} 1862 1863@book{suppes72, 1864 author = {Patrick Suppes}, 1865 title = {Axiomatic Set Theory}, 1866 year = 1972, 1867 publisher = {Dover}} 1868 1869@inproceedings{sutcliffe-2000, 1870 author = "Geoff Sutcliffe", 1871 title = "System Description: {SystemOnTPTP}", 1872 editor = "David McAllester", 1873 booktitle = {Automated Deduction --- {CADE}-17 International Conference}, 1874 series = "Lecture Notes in Artificial Intelligence", 1875 volume = {1831}, 1876 pages = "406--410", 1877 year = 2000, 1878 publisher = Springer} 1879 1880@misc{tofof, 1881 author = "Geoff Sutcliffe", 1882 title = "{ToFoF}", 1883 note = "\url{http://www.cs.miami.edu/~tptp/ATPSystems/ToFoF/}"} 1884 1885@Article{Sutter:2005, 1886 author = {H. Sutter}, 1887 title = {The Free Lunch Is Over --- A Fundamental Turn Toward Concurrency in Software}, 1888 journal = {Dr. Dobb's Journal}, 1889 year = 2005, 1890 volume = 30, 1891 number = 3} 1892 1893@InCollection{szasz93, 1894 author = {Nora Szasz}, 1895 title = {A Machine Checked Proof that {Ackermann's} Function is not 1896 Primitive Recursive}, 1897 crossref = {huet-plotkin93}, 1898 pages = {317-338}} 1899 1900@TechReport{Syme:1997:DECLARE, 1901 author = {D. Syme}, 1902 title = {{DECLARE}: A Prototype Declarative Proof System for Higher Order Logic}, 1903 institution = {University of Cambridge Computer Laboratory}, 1904 year = 1997, 1905 number = 416 1906} 1907 1908@PhdThesis{Syme:1998:thesis, 1909 author = {D. Syme}, 1910 title = {Declarative Theorem Proving for Operational Semantics}, 1911 school = {University of Cambridge}, 1912 year = 1998, 1913 note = {Submitted} 1914} 1915 1916@InProceedings{Syme:1999:TPHOL, 1917 author = {D. Syme}, 1918 title = {Three Tactic Theorem Proving}, 1919 crossref = {tphols99}} 1920 1921%T 1922 1923@book{takeuti87, 1924 author = {G. Takeuti}, 1925 title = {Proof Theory}, 1926 year = 1987, 1927 publisher = NH, 1928 edition = {2nd}} 1929 1930@Book{thompson91, 1931 author = {Simon Thompson}, 1932 title = {Type Theory and Functional Programming}, 1933 publisher = {Addison-Wesley}, 1934 year = 1991} 1935 1936@book{Thompson-Haskell,author={Simon Thompson}, 1937title={Haskell: The Craft of Functional Programming}, 1938publisher={Addison-Wesley},year=1999} 1939 1940@misc{kodkod-2009, 1941 author = "Emina Torlak", 1942 title = {Kodkod: Constraint Solver for Relational Logic}, 1943 note = "\url{http://alloy.mit.edu/kodkod/}"} 1944 1945@misc{kodkod-2009-options, 1946 author = "Emina Torlak", 1947 title = "Kodkod {API}: Class {Options}", 1948 note = "\url{http://alloy.mit.edu/kodkod/docs/kodkod/engine/config/Options.html}"} 1949 1950@inproceedings{torlak-jackson-2007, 1951 title = "Kodkod: A Relational Model Finder", 1952 author = "Emina Torlak and Daniel Jackson", 1953 editor = "Orna Grumberg and Michael Huth", 1954 booktitle = "TACAS 2007", 1955 series = LNCS, 1956 volume = {4424}, 1957 pages = "632--647", 1958 year = 2007, 1959 publisher = Springer} 1960 1961@inproceedings{traytel-berghofer-nipkow-2011, 1962 author = {Dmitriy Traytel and Stefan Berghofer and Tobias Nipkow}, 1963 title = {{Extending Hindley-Milner Type Inference with Coercive Structural Subtyping}}, 1964 year = 2011, 1965 editor = {Hongseok Yang}, 1966 booktitle = "APLAS 2011", 1967 series = LNCS, 1968 volume = {7078}, 1969 pages = "89--104"} 1970 1971@inproceedings{traytel-et-al-2012, 1972 author = "Dmitriy Traytel and Andrei Popescu and Jasmin Christian Blanchette", 1973 title = {Foundational, Compositional (Co)datatypes for Higher-Order 1974 Logic---{C}ategory Theory Applied to Theorem Proving}, 1975 year = {2012}, 1976 pages = {596--605}, 1977 booktitle = {27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012}, 1978 publisher = {IEEE} 1979} 1980 1981@Unpublished{Trybulec:1993:MizarFeatures, 1982 author = {A. Trybulec}, 1983 title = {Some Features of the {Mizar} Language}, 1984 note = {Presented at a workshop in Turin, Italy}, 1985 year = 1993 1986} 1987 1988%V 1989 1990@Unpublished{voelker94, 1991 author = {Norbert V{\"o}lker}, 1992 title = {The Verification of a Timer Program using {Isabelle/HOL}}, 1993 note = {\url{ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}}, 1994 year = 1994, 1995 month = aug} 1996 1997%W 1998 1999@inproceedings{wadler89how, 2000 author = {P. Wadler and S. Blott}, 2001 title = {How to make ad-hoc polymorphism less ad-hoc}, 2002 booktitle = {ACM Symp.\ Principles of Programming Languages}, 2003 year = 1989 2004} 2005 2006@phdthesis{weber-2008, 2007 author = "Tjark Weber", 2008 title = "SAT-Based Finite Model Generation for Higher-Order Logic", 2009 school = {Dept.\ of Informatics, T.U. M\"unchen}, 2010 type = "{Ph.D.}\ thesis", 2011 year = 2008} 2012 2013@Misc{x-symbol, 2014 author = {Christoph Wedler}, 2015 title = {Emacs package ``{X-Symbol}''}, 2016 note = {\url{http://x-symbol.sourceforge.net}} 2017} 2018 2019@misc{weidenbach-et-al-2009, 2020 author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski", 2021 title = "{SPASS} Version 3.5", 2022 note = {\url{http://www.spass-prover.org/publications/spass.pdf}}} 2023 2024@manual{isabelle-system, 2025 author = {Makarius Wenzel}, 2026 title = {The {Isabelle} System Manual}, 2027 note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}} 2028 2029@manual{isabelle-jedit, 2030 author = {Makarius Wenzel}, 2031 title = {{Isabelle/jEdit}}, 2032 note = {\url{https://isabelle.in.tum.de/doc/jedit.pdf}}} 2033 2034@manual{isabelle-isar-ref, 2035 author = {Makarius Wenzel}, 2036 title = {The {Isabelle/Isar} Reference Manual}, 2037 note = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}} 2038 2039@manual{isabelle-implementation, 2040 author = {Makarius Wenzel}, 2041 title = {The {Isabelle/Isar} Implementation}, 2042 note = {\url{https://isabelle.in.tum.de/doc/implementation.pdf}}} 2043 2044@InProceedings{Wenzel:1999:TPHOL, 2045 author = {Markus Wenzel}, 2046 title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, 2047 crossref = {tphols99}} 2048 2049@InProceedings{Wenzel:1997:TPHOL, 2050 author = {Markus Wenzel}, 2051 title = {Type Classes and Overloading in Higher-Order Logic}, 2052 crossref = {tphols97}} 2053 2054@phdthesis{Wenzel-PhD, 2055 author={Markus Wenzel}, 2056 title={Isabelle/Isar --- a versatile environment for human-readable formal proof documents}, 2057 school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}, 2058 year=2002, 2059 note = {\url{https://mediatum.ub.tum.de/doc/601724/601724.pdf}}} 2060 2061@Article{Wenzel-Wiedijk:2002, 2062 author = {Freek Wiedijk and Markus Wenzel}, 2063 title = {A comparison of the mathematical proof languages {Mizar} and {Isar}.}, 2064 journal = {Journal of Automated Reasoning}, 2065 year = 2002, 2066 volume = 29, 2067 number = {3-4} 2068} 2069 2070@InCollection{Wenzel-Paulson:2006, 2071 author = {Markus Wenzel and Lawrence C. Paulson}, 2072 title = {{Isabelle/Isar}}, 2073 booktitle = {The Seventeen Provers of the World}, 2074 year = 2006, 2075 editor = {F. Wiedijk}, 2076 series = {LNAI 3600}, 2077 publisher = Springer 2078} 2079 2080@InCollection{Wenzel:2006:Festschrift, 2081 author = {Makarius Wenzel}, 2082 title = {{Isabelle/Isar} --- a generic framework for human-readable proof documents}, 2083 booktitle = {From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec}, 2084 publisher = {University of Bia{\l}ystok}, 2085 year = 2007, 2086 editor = {R. Matuszewski and A. Zalewska}, 2087 volume = {10(23)}, 2088 series = {Studies in Logic, Grammar, and Rhetoric}, 2089 note = {\url{http://www.in.tum.de/~wenzelm/papers/isar-framework.pdf}} 2090} 2091 2092@InProceedings{Wenzel-Chaieb:2007b, 2093 author = {Makarius Wenzel and Amine Chaieb}, 2094 title = {{SML} with antiquotations embedded into {Isabelle/Isar}}, 2095 booktitle = {Workshop on Programming Languages for Mechanized Mathematics 2096 (satellite of CALCULEMUS 2007). Hagenberg, Austria}, 2097 editor = {Jacques Carette and Freek Wiedijk}, 2098 month = {June}, 2099 year = {2007} 2100} 2101 2102@InProceedings{Wenzel:2009, 2103 author = {M. Wenzel}, 2104 title = {Parallel Proof Checking in {Isabelle/Isar}}, 2105 booktitle = {ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009)}, 2106 year = 2009, 2107 editor = {Dos Reis, G. and L. Th\'ery}, 2108 publisher = {ACM Digital Library}} 2109 2110@InProceedings{Wenzel:2010, 2111 author = {Makarius Wenzel}, 2112 title = {Asynchronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}}, 2113 booktitle = {User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite Workshop}, 2114 year = 2010, 2115 editor = {C. Sacerdoti Coen and D. Aspinall}, 2116 series = {ENTCS}, 2117 month = {July}, 2118 publisher = {Elsevier}, 2119 url = {http://www.lri.fr/~wenzel/papers/async-isabelle-scala.pdf}} 2120 2121@InProceedings{Wenzel:2011:CICM, 2122 author = {M. Wenzel}, 2123 title = {Isabelle as Document-oriented Proof Assistant}, 2124 editor = {J. H. Davenport and W. M. Farmer and F. Rabe and J. Urban}, 2125 booktitle = {Conference on Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011)}, 2126 year = 2011, 2127 volume = {6824}, 2128 series = {LNAI}, 2129 publisher = {Springer}} 2130 2131@InProceedings{Wenzel:2012, 2132 author = {Makarius Wenzel}, 2133 title = {{Isabelle/jEdit} --- a {Prover IDE} within the {PIDE} framework}, 2134 booktitle = {Conference on Intelligent Computer Mathematics (CICM 2012)}, 2135 year = 2012, 2136 editor = {J. Jeuring and others}, 2137 volume = 7362, 2138 series = {LNAI}, 2139 publisher = {Springer}} 2140 2141@InProceedings{Wenzel:2012:UITP-EPTCS, 2142 author = {Makarius Wenzel}, 2143 title = {{READ-EVAL-PRINT} in Parallel and Asynchronous Proof-checking}, 2144 booktitle = {User Interfaces for Theorem Provers (UITP 2012)}, 2145 year = 2013, 2146 series = {EPTCS} 2147} 2148 2149@inproceedings{Wenzel:2013:ITP, 2150 author = {Makarius Wenzel}, 2151 title = {Shared-Memory Multiprocessing for Interactive Theorem Proving}, 2152 booktitle = {Interactive Theorem Proving --- 4th International Conference, 2153 ITP 2013, Rennes, France, July 22-26, 2013. Proceedings}, 2154 editor = {Sandrine Blazy and 2155 Christine Paulin-Mohring and 2156 David Pichardie}, 2157 year = {2013}, 2158 ee = {https://doi.org/10.1007/978-3-642-39634-2_30}, 2159 publisher = {Springer}, 2160 series = {Lecture Notes in Computer Science}, 2161 volume = {7998}, 2162} 2163 2164@inproceedings{Wenzel:2014:ITP-PIDE, 2165 author = {Makarius Wenzel}, 2166 title = {Asynchronous User Interaction and Tool Integration in {Isabelle/PIDE}}, 2167 booktitle = {5th International Conference on Interactive Theorem Proving, ITP 2014}, 2168 editor = {Gerwin Klein and Ruben Gamboa}, 2169 year = {2014}, 2170 publisher = {Springer}, 2171 series = {Lecture Notes in Computer Science}, 2172 volume = {8558}, 2173} 2174 2175@InProceedings{Wenzel:2014:UITP, 2176 author = {Makarius Wenzel}, 2177 title = {System description: {Isabelle/jEdit} in 2014}, 2178 booktitle = {User Interfaces for Theorem Provers (UITP 2014)}, 2179 editor = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo, Bruno}, 2180 year = 2014, 2181 series = {EPTCS}, 2182 month = {July}, 2183 note = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?UITP2014:11}} 2184} 2185 2186@book{principia, 2187 author = {A. N. Whitehead and B. Russell}, 2188 title = {Principia Mathematica}, 2189 year = 1962, 2190 publisher = CUP, 2191 note = {Paperback edition to *56, 2192 abridged from the 2nd edition (1927)}} 2193 2194@Misc{Wiedijk:1999:Mizar, 2195 author = {Freek Wiedijk}, 2196 title = {Mizar: An Impression}, 2197 howpublished = {Unpublished paper}, 2198 year = 1999, 2199 note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz}} 2200} 2201 2202@Misc{Wiedijk:2000:MV, 2203 author = {Freek Wiedijk}, 2204 title = {The Mathematical Vernacular}, 2205 howpublished = {Unpublished paper}, 2206 year = 2000, 2207 note = {\url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}} 2208} 2209 2210@misc{wikipedia-2009-aa-trees, 2211 key = "Wikipedia", 2212 title = "Wikipedia: {AA} Tree", 2213 note = "\url{http://en.wikipedia.org/wiki/AA_tree}"} 2214 2215@book{winskel93, 2216 author = {Glynn Winskel}, 2217 title = {The Formal Semantics of Programming Languages}, 2218 publisher = MIT,year=1993} 2219 2220@InCollection{wos-bledsoe, 2221 author = {Larry Wos}, 2222 title = {Automated Reasoning and {Bledsoe's} Dream for the Field}, 2223 crossref = {bledsoe-fest}, 2224 pages = {297-342}} 2225 2226@InProceedings{Zammit:1999:TPHOL, 2227 author = {Vincent Zammit}, 2228 title = {On the Implementation of an Extensible Declarative Proof Language}, 2229 crossref = {tphols99}} 2230 2231%Z 2232 2233@misc{z3, 2234 key = "Z3", 2235 title = "Z3: An Efficient {SMT} Solver", 2236 note = "\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}"} 2237 2238 2239% CROSS REFERENCES 2240 2241@book{handbk-lics2, 2242 editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum}, 2243 title = {Handbook of Logic in Computer Science}, 2244 booktitle = {Handbook of Logic in Computer Science}, 2245 publisher = {Oxford University Press}, 2246 year = 1992, 2247 volume = 2} 2248 2249@book{types93, 2250 editor = {Henk Barendregt and Tobias Nipkow}, 2251 title = TYPES # {: International Workshop {TYPES '93}}, 2252 booktitle = TYPES # {: International Workshop {TYPES '93}}, 2253 year = {published 1994}, 2254 publisher = {Springer}, 2255 series = {LNCS 806}} 2256 2257@book{barwise-handbk, 2258 editor = {J. Barwise}, 2259 title = {Handbook of Mathematical Logic}, 2260 booktitle = {Handbook of Mathematical Logic}, 2261 year = 1977, 2262 publisher = NH} 2263 2264@Proceedings{tlca93, 2265 title = {Typed Lambda Calculi and Applications}, 2266 booktitle = {Typed Lambda Calculi and Applications}, 2267 editor = {M. Bezem and J.F. Groote}, 2268 year = 1993, 2269 publisher = {Springer}, 2270 series = {LNCS 664}} 2271 2272@book{birtwistle89, 2273 editor = {Graham Birtwistle and P. A. Subrahmanyam}, 2274 title = {Current Trends in Hardware Verification and Automated 2275 Theorem Proving}, 2276 booktitle = {Current Trends in Hardware Verification and Automated 2277 Theorem Proving}, 2278 publisher = {Springer}, 2279 year = 1989} 2280 2281@book{bledsoe-fest, 2282 title = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}}, 2283 booktitle = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}}, 2284 publisher = {Kluwer Academic Publishers}, 2285 year = 1991, 2286 editor = {Robert S. Boyer}} 2287 2288@Proceedings{cade12, 2289 editor = {Alan Bundy}, 2290 title = {Automated Deduction --- {CADE}-12 2291 International Conference}, 2292 booktitle = {Automated Deduction --- {CADE}-12 2293 International Conference}, 2294 year = 1994, 2295 series = {LNAI 814}, 2296 publisher = {Springer}} 2297 2298@book{types94, 2299 editor = {Peter Dybjer and Bengt Nordstr{{\"o}m} and Jan Smith}, 2300 title = TYPES # {: International Workshop {TYPES '94}}, 2301 booktitle = TYPES # {: International Workshop {TYPES '94}}, 2302 year = 1995, 2303 publisher = {Springer}, 2304 series = {LNCS 996}} 2305 2306@book{huet-plotkin91, 2307 editor = {{G{\'e}rard} Huet and Gordon Plotkin}, 2308 title = {Logical Frameworks}, 2309 booktitle = {Logical Frameworks}, 2310 publisher = CUP, 2311 year = 1991} 2312 2313@book{huet-plotkin93, 2314 editor = {{G{\'e}rard} Huet and Gordon Plotkin}, 2315 title = {Logical Environments}, 2316 booktitle = {Logical Environments}, 2317 publisher = CUP, 2318 year = 1993} 2319 2320@Proceedings{hug93, 2321 editor = {J. Joyce and C. Seger}, 2322 title = {Higher Order Logic Theorem Proving and Its 2323 Applications: HUG '93}, 2324 booktitle = {Higher Order Logic Theorem Proving and Its 2325 Applications: HUG '93}, 2326 year = {Published 1994}, 2327 publisher = {Springer}, 2328 series = {LNCS 780}} 2329 2330@proceedings{colog88, 2331 editor = {P. Martin-L{\"o}f and G. Mints}, 2332 title = {COLOG-88: International Conference on Computer Logic}, 2333 booktitle = {COLOG-88: International Conference on Computer Logic}, 2334 year = {Published 1990}, 2335 publisher = {Springer}, 2336 organization = {Estonian Academy of Sciences}, 2337 address = {Tallinn}, 2338 series = {LNCS 417}} 2339 2340@book{odifreddi90, 2341 editor = {P. Odifreddi}, 2342 title = {Logic and Computer Science}, 2343 booktitle = {Logic and Computer Science}, 2344 publisher = {Academic Press}, 2345 year = 1990} 2346 2347@proceedings{extensions91, 2348 editor = {Peter Schroeder-Heister}, 2349 title = {Extensions of Logic Programming}, 2350 booktitle = {Extensions of Logic Programming}, 2351 year = 1991, 2352 series = {LNAI 475}, 2353 publisher = {Springer}} 2354 2355@proceedings{cade10, 2356 editor = {Mark E. Stickel}, 2357 title = {10th } # CADE, 2358 booktitle = {10th } # CADE, 2359 year = 1990, 2360 publisher = {Springer}, 2361 series = {LNAI 449}} 2362 2363@Proceedings{lics8, 2364 editor = {M. Vardi}, 2365 title = {Eighth Annual Symposium on Logic in Computer Science}, 2366 booktitle = {Eighth Annual Symposium on Logic in Computer Science}, 2367 publisher = IEEE, 2368 year = 1993} 2369 2370@book{wos-fest, 2371 title = {Automated Reasoning and its Applications: 2372 Essays in Honor of {Larry Wos}}, 2373 booktitle = {Automated Reasoning and its Applications: 2374 Essays in Honor of {Larry Wos}}, 2375 publisher = MIT, 2376 year = 1997, 2377 editor = {Robert Veroff}} 2378 2379@proceedings{fme93, 2380 editor = {J. C. P. Woodcock and P. G. Larsen}, 2381 title = {FME '93: Industrial-Strength Formal Methods}, 2382 booktitle = {FME '93: Industrial-Strength Formal Methods}, 2383 year = 1993, 2384 publisher = Springer, 2385 series = LNCS, 2386 volume = 670} 2387 2388@Proceedings{tphols96, 2389 title = {Theorem Proving in Higher Order Logics: {TPHOLs} '96}, 2390 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '96}, 2391 editor = {J. von Wright and J. Grundy and J. Harrison}, 2392 publisher = Springer, 2393 series = LNCS, 2394 volume = 1125, 2395 year = 1996} 2396 2397@Proceedings{tphols97, 2398 title = {Theorem Proving in Higher Order Logics: {TPHOLs} '97}, 2399 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '97}, 2400 editor = {Elsa L. Gunter and Amy Felty}, 2401 publisher = Springer, 2402 series = LNCS, 2403 volume = 1275, 2404 year = 1997} 2405 2406@Proceedings{tphols98, 2407 title = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, 2408 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, 2409 editor = {Jim Grundy and Malcom Newey}, 2410 publisher = Springer, 2411 series = LNCS, 2412 volume = 1479, 2413 year = 1998} 2414 2415@Proceedings{tphols99, 2416 title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, 2417 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, 2418 editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and 2419 Paulin, C. and Thery, L.}, 2420 publisher = Springer, 2421 series = LNCS, 2422 volume = 1690, 2423 year = 1999} 2424 2425@Proceedings{tphols2000, 2426 title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000}, 2427 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000}, 2428 editor = {J. Harrison and M. Aagaard}, 2429 publisher = Springer, 2430 series = LNCS, 2431 volume = 1869, 2432 year = 2000} 2433 2434@Proceedings{tphols2001, 2435 title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001}, 2436 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001}, 2437 editor = {R. J. Boulton and P. B. Jackson}, 2438 publisher = Springer, 2439 series = LNCS, 2440 volume = 2152, 2441 year = 2001} 2442 2443@Proceedings{ijcar2006, 2444 title = {Automated Reasoning: {IJCAR} 2006}, 2445 booktitle = {Automated Reasoning: {IJCAR} 2006}, 2446 editor = {U. Furbach and N. Shankar}, 2447 publisher = Springer, 2448 series = LNCS, 2449 volume = 4130, 2450 year = 2006} 2451 2452@Proceedings{tphols2007, 2453 title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007}, 2454 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007}, 2455 editor = {K. Schneider and J. Brandt}, 2456 publisher = Springer, 2457 series = LNCS, 2458 volume = 4732, 2459 year = 2007} 2460 2461@Proceedings{tphols2008, 2462 title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008}, 2463 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008}, 2464 editor = {Otmane A{\"{\i}}t Mohamed and C{\'{e}}sar A. Mu{\~{n}}oz and 2465 Sofi{\`{e}}ne Tahar}, 2466 publisher = Springer, 2467 series = LNCS, 2468 year = 2008} 2469% editor = 2470% volume = 4732, 2471 2472@Proceedings{itp2010, 2473 title = {Interactive Theorem Proving: {ITP}-10}, 2474 booktitle = {Interactive Theorem Proving: {ITP}-10}, 2475 editor = "Matt Kaufmann and Lawrence Paulson", 2476 publisher = Springer, 2477 series = LNCS, 2478 year = 2010} 2479 2480@unpublished{classes_modules, 2481 title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison}, 2482 author = {Stefan Wehr and Manuel M. T. Chakravarty}, 2483 note = {\url{https://www.cse.unsw.edu.au/~chak/papers/modules-classes.pdf}} 2484} 2485 2486@inproceedings{runciman-naylor-lindblad, 2487 author = {Runciman, Colin and Naylor, Matthew and Lindblad, Fredrik}, 2488 title = {Smallcheck and {Lazy Smallcheck}: Automatic Exhaustive Testing for Small Values}, 2489 booktitle = {Proceedings of the First ACM SIGPLAN Symposium on Haskell (Haskell 2008)}, 2490 year = {2008}, 2491 pages = {37--48}, 2492 publisher = {ACM}, 2493} 2494 2495