@String{AP   = {Ann. Phys.}}

@Book{1979_Adams,
  author =	 {Douglas Adams},
  editor =	 { },
  title =	 {The Hitchhiker's Guide to the Galaxy},
  publisher =	 {},
  year =	 1979,
  address =	 {London, UK},
}

@Article{1905_Einstein,
  author =	 {Albert Einstein},
  title =	 {{\"U}ber die von der molekularkinetischen Theorie
                  der W{\"a}rme geforderte Bewegung von in ruhenden
                  Fl{\"u}ssigkeiten suspendierten Teilchen},
  journal =	 AP,
  year =	 1905,
  volume =	 17,
  pages =	 {549--560}
}

@phdthesis{benthem-jutting-1977,
  author = "van Benthem Jutting, Lambert S.",
  title = "Checking {L}andau's ``{G}rundlagen'' in the {A}utomath System",
  school = "Technische Hogeschool Eindhoven",
  year = 1977,
  note = "DOI: 10.6100/IR23183"}

@article{hales-et-al-2015,
  author    = {Thomas C. Hales and
               Mark Adams and
               Gertrud Bauer and
               Dat Tat Dang and
               John Harrison and
               Truong Le Hoang and
               Cezary Kaliszyk and
               Victor Magron and
               Sean McLaughlin and
               Thang Tat Nguyen and
               Truong Quang Nguyen and
               Tobias Nipkow and
               Steven Obua and
               Joseph Pleso and
               Jason M. Rute and
               Alexey Solovyev and
               An Hoai Thi Ta and
               Trung Nam Tran and
               Diep Thi Trieu and
               Josef Urban and
               Ky Khac Vu and
               Roland Zumkeller},
  title     = {A formal proof of the {K}epler conjecture},
  journal   = {CoRR},
  volume    = {abs/1501.02155},
  year      = {2015},
  XXXurl       = {http://arxiv.org/abs/1501.02155},
  XXXeprinttype = {arXiv},
  XXXeprint    = {1501.02155},
  note = "DOI: 10.48550/arXiv.1501.02155"
}

@article{hurd-2003-prob,
  author    = {Joe Hurd},
  title     = {Verification of the Miller-Rabin probabilistic primality test},
  journal   = {J. Logic and Algebraic Programming},
  volume    = {56},
  number    = {1--2},
  pages     = {3--21},
  year      = {2003}
}

@book{nipkow-klein-2014,
  author    = {Tobias Nipkow and
               Gerwin Klein},
  title     = {Concrete Semantics:\ With {Isabelle/HOL}},
  publisher = {Springer},
  year      = {2014}
}

@inproceedings{sewell-et-al-2011,
  author    = {Thomas Sewell and
               Simon Winwood and
               Peter Gammie and
               Toby C. Murray and
               June Andronick and
               Gerwin Klein},
  title     = {{seL4} Enforces Integrity},
  booktitle = "Interactive Theorem Proving (ITP 2011\/)",
  pages     = {325--340},
  year      = {2011},
  editor    = {Marko C. J. D. van~Eekelen and
               Herman Geuvers and
               Julien Schmaltz and
               Freek Wiedijk},
  series    = {Lecture Notes in Computer Science},
  volume    = {6898},
  publisher = {Springer}
}

@incollection{andrews-2001,
  author    = {Peter B. Andrews},
  title     = {Classical Type Theory},
  booktitle = {Handbook of Automated Reasoning},
  volume = 2,
  pages     = {965--1007},
  year      = {2001},
  editor    = {John Alan Robinson and
               Andrei Voronkov},
  publisher = {Elsevier and {MIT} Press}
}

@inproceedings{lochbihler-2012,
  author    = {Andreas Lochbihler},
  title     = {{J}ava and the {J}ava Memory Model---{A} Unified, Machine-Checked
               Formalisation},
  booktitle = {ESOP 2012},
  year      = {2012},
  pages     = {497--517},
  editor    = {Helmut Seidl},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7211},
}

@techreport{snow,
  author = {Andrew J. Carlson and Chad M. Cumby and Jeff L. Rosen and Dan Roth},
  title = {{SNoW} User Guide},
  year = {1999},
  institution = {C.S. Dept., University of Illinois at Urbana-Champaign},
  xxxnumber = {UIUCDCS-R-99-2101},
  url = "http://cogcomp.cs.illinois.edu/papers/CCRR99.pdf",
}

@article{meng-paulson-2008-trans,
  author = {Jia Meng and Lawrence C. Paulson},
  title = {Translating Higher-Order Clauses to First-Order Clauses},
  journal = {J.~Automated Reasoning},
  volume = 40,
  number = 1,
  pages = {35--60},
  year = 2008}

@phdthesis{popescu-2010-thesis,
  author = "Andrei Popescu",
  title = "Contributions to the Theory of Syntax with Bindings and to Process Algebra",
  school = {C.S.\ Dept., University of Illinois at Urbana-Champaign},
  type = "{Ph.D.}\ thesis",
  year = 2010}
% \href{http://hdl.handle.net/2142/18477}
{\nolinkurl{hdl.handle.net/2142/18477}}

@inproceedings{claessen-et-al-2011,
  title = "Sort It Out with Monotonicity\dash {T}ranslating between Many-Sorted and
  Unsorted First-Order Logic",
  author = "Koen Claessen and Ann Lilliestr{\"o}m and Nicholas Smallbone",
  editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
  booktitle = {CADE 2011},
  year = 2011,
  series = "Lecture Notes in Computer Science",
  volume = "6803",
  pages = "207--221",
  publisher = "Springer"}

@article{claessen-lilliestrom-2011,
  author = "Koen Claessen and Ann Lilliestr{\"o}m",
  title = "Automated Inference of Finite Unsatisfiability",
  journal = {J.~Automated Reasoning},
  volume = "47",
  number = "2",
  pages = "111--132",
  year = 2011}

@article{blanchette-et-al-2013-smt,
  author = {Jasmin Christian Blanchette and Sascha B{\"o}hme and Lawrence C. Paulson},
  title = "Extending {S}ledgehammer with {SMT} Solvers",
  journal = "Journal of Automated Reasoning",
  volume = 51,
  number = 1,
  pages = "109--128",
  year = 2013}

@inproceedings{blanchette-et-al-2013-types,
  author = {J. C. Blanchette and Sascha B\"ohme and Andrei Popescu and Nicholas Smallbone},
  title = "Encoding Monomorphic and Polymorphic Types",
  booktitle = "TACAS 2013",
  editor = "Nir Piterman and Scott Smolka",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  pages     = {493--507},
  volume    = {7795},
  year = {2013},
  note = {DOI: 10.1007/978-3-642-36742-7\_34},
}

@article{urban-2006,
  author = {Josef Urban},
  title = {{MPTP} 0.2: Design, Implementation, and Initial Experiments},
  journal = {J.~Automated Reasoning},
  volume = 37,
  number = "\hbox{1--2}",
  pages = {21--43},
  year = 2006}

@inproceedings{couchot-lescuyer-2007,
  author    = {Jean-Fran\c{c}ois Couchot and St{\'e}phane Lescuyer},
  title     = {Handling Polymorphism in Automated Deduction},
  booktitle = {CADE 2007},
  editor    = {Frank Pfenning},
  series    = {Lecture Notes in Computer Science},
  volume    = {4603},
  publisher = {Springer},
  year      = {2007},
  pages     = {263--278},
}

@inproceedings{leino-ruemmer-2010,
  author    = {K. Rustan M. Leino and Philipp R{\"u}mmer},
  title     = {A Polymorphic Intermediate Verification Language:
               Design and Logical Encoding},
  booktitle = {TACAS 2010},
  editor    = {Javier Esparza and Rupak Majumdar},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6015},
  year      = {2010},
  pages     = {312--327},
}

@article{riazanov-voronkov-2002,
  author = "Alexander Riazanov and Andrei Voronkov",
  title = "The Design and Implementation of {Vampire}",
  journal = "AI Comm.",
  year = 2002,
  volume = 15,
  number ="\hbox{2-3}",
  pages = "91--110"}

@inproceedings{de-moura-bjoerner-2008-z3,
  author    = {de Moura, Leonardo and Nikolaj Bj{\o}rner},
  title     = {{Z3}: {An} Efficient {SMT} Solver},
  editor = "C. R. Ramakrishnan and Jakob Rehof",
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems ({TACAS} 2008\/)},
  volume    = {4963},
  series    = "Lecture Notes in Computer Science",
  pages     = {337--340},
  publisher = {Springer},
  year      = {2008},
  note = "DOI: 10.1007/978-3-540-78800-3\_24"
}

@inproceedings{schulz-2004,
  author = "Stephan Schulz",
  title = "System Description: {E~0.81}",
  booktitle = "International Joint Conference on Automated Reasoning (IJCAR 2004)",
  editor = "David Basin and Micha{\"e}l Rusinowitch",
  publisher="Springer",
  series={{Lecture Notes in Computer Science}},
  volume = 3097,
  pages = "223--228",
  year = 2004}

@inproceedings{barnett-et-al-2006,
  title = "{B}oogie: A Modular Reusable Verifier for Object-Oriented Programs",
  author = "Mike Barnett and Bor-Yuh Evan Chang and Robert DeLine and Bart Jacobs and K. Rustan M. Leino",
  editor    = {Frank S. de~Boer and
               Marcello M. Bonsangue and
               Susanne Graf and
               Willem-Paul de~Roever},
  booktitle = "FMCO 2005",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume = 4111,
  pages = "364--387",
  year = 2006}

@inproceedings{bobot-et-al-2011,
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
  title = {{Why3}: Shepherd Your Herd of Provers},
  editor = "K. Rustan M. Leino and Micha\l{} Moskal",
  booktitle = {Boogie 2011},
  pages = "53--64",
  year = 2011
}

@article{matuszewski-rudnicki-2005,
  title = "{Mizar}: The first 30 years",
  author = "Roman Matuszewski and Piotr Rudnicki",
  journal = "Mechanized Mathematics and Its Applications",
  volume = 4,
  number = 1,
  year = 2005,
  pages = "3--24"}

@book{nipkow-et-al-2002,
  author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
  title = "{I}sabelle/{HOL}: A Proof Assistant for Higher-Order Logic",
  publisher="Springer",
  series={{Lecture Notes in Computer Science}},
  volume={2283},
  year=2002,
  note = "DOI: 10.1007/3-540-45949-9"}

@inproceedings{blanchette-nipkow-2010,
  title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
  author = "J. C. Blanchette and Tobias Nipkow",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  year = 2010,
  editor = "Matt Kaufmann and Lawrence C. Paulson",
  booktitle = "Interactive Theorem Proving (ITP 2010\/)",
  volume = 6172,
  pages = "131--146"}

@article{blanchette-krauss-2011,
  title = "Monotonicity Inference for Higher-Order Formulas",
  author = "J. C. Blanchette and Alexander Krauss",
  number = 4,
  volume = 47,
  year = 2011,
  pages = "369--398",
  journal = "Journal of Automated Reasoning"}

@misc{sutcliffe-tptp-xxx,
  title = "The {TPTP} Problem Library: {TPTP} v5.0.0",
  author = "Geoff Sutcliffe",
  note = "\href{http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml}
{\nolinkurl{www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml}}"}

@article{sutcliffe-tptp,
  author = "Geoff Sutcliffe",
  title = "The {TPTP} Problem Library and Associated Infrastructure---{T}he {FOF} and {CNF} Parts, v3.5.0",
  journal = "Journal of Automated Reasoning",
  volume = "43",
  number = 4,
  pages = "337--362",
  year = 2009}

@inproceedings{sutcliffe-et-al-2012-tff,
  author = "Geoff Sutcliffe and Stephan Schulz and Koen Claessen and Peter Baumgartner",
  title = "The {TPTP} typed first-order form with arithmetic",
  booktitle = "LPAR-18",
  editor = "Nikolaj Bj{\o}rner and Andrei Voronkov",
  publisher = "Springer",
  pages     = {406--419},
  series    = {Lecture Notes in Computer Science},
  volume    = {7180},
  year = "2012"}  

%  year = 2011}
% note = "Available at \href{https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa/TFFArith.pdf}
{\nolinkurl{https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa/TFFArith.pdf}}",

@inproceedings{blanchette-paskevich-2013,
  author = "J. C. Blanchette and Andrei Paskevich",
  title = "{TFF1}: The {TPTP} typed first-order form with rank-1 polymorphism",
  editor = "Maria Paola Bonacina",
  booktitle = "CADE 2013",
  series = "Lecture Notes in Computer Science",
  volume = 7898,
  pages = "414--420",
  publisher = "Springer",
  year = 2013}

@inproceedings{paulson-susanto-2007,
  author = {Lawrence C. Paulson and Kong Woei Susanto},
  booktitle = {TPHOLs 2007},
  editor = {Klaus Schneider and Jens Brandt},
  title = {Source-Level Proof Reconstruction for Interactive Theorem Proving},
  pages = {232--245},
  series = {{Lecture Notes in Computer Science}},
  publisher = {Springer},
  volume = {4732},
  year = {2007}}

@article{sutcliffe-2013-casc-j6,
    author       = "Sutcliffe, Geoff",
    title = "The 6th {IJCAR} Automated Theorem Proving System Competition---{CASC}-{J6}",
    journal = "AI Comm.",
    volume = 26,
    number = 2,
    pages = "211--223",
    year = 2013}

@inproceedings{sutcliffe-2012-casc-j6,
  author    = {Geoff Sutcliffe},
  title     = {Proceedings of the 6th {IJCAR} {ATP} System Competition (CASC-J6\/)},
  booktitle = "{CASC-J6}",
  editor    = {Geoff Sutcliffe},
  series    = {EPiC},
  volume    = {11},
  pages     = {1--50},
  year      = {2012},
  publisher = {EasyChair}
}

@article{stickel-1986,
  author = {Mark E. Stickel},
  title = {Schubert's Steamroller Problem: Formulations and Solutions},
  journal = {J.~Automated Reasoning},
  volume = 2,
  number = 1,
  pages = {89--101},
  year = 1986}

@book{enderton-1972,
  title = "A Mathematical Introduction to Logic",
  author = "Herbert B. Enderton",
  publisher = "Academic Press",
  year = 1972}

@article{wick-mccune-1989,
  author = "Cynthia A. Wick and William W. McCune",
  title = "Automated reasoning about elementary point-set topology",
  journal = {J.~Automated Reasoning},
  volume = 5,
  number = 2,
  pages = "239--255",
  year = 1989}

@misc{ranise-tinelli-2006,
  author = "Silvio Ranise and Cesare Tinelli",
  title = "The {SMT-LIB} Standard: Version 1.2",
  note = "Available at \href{http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf}
{\nolinkurl{goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf}}",
  year = 2006}

@InProceedings{barrett-et-al-2010,
  author = {Clark Barrett and Aaron Stump and Cesare Tinelli},
  title =	 {The {SMT-LIB} Standard---{V}ersion 2.0},
  year =	 2010,
  booktitle = {SMT 2010},
  editor =	 {A. Gupta and D. Kroening}
}

@inproceedings{bobot-et-al-2008,
  author = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean and St\'ephane Lescuyer},
  title = {Implementing Polymorphism in {SMT} Solvers},
  booktitle = {SMT 2008},
  year = 2008,
  editor = {Clark Barrett and de Moura, Leonardo}}

@article{meng-paulson-2009-relev,
  author = {Jia Meng and Lawrence C. Paulson},
  title = {Lightweight Relevance Filtering for Machine-Generated Resolution Problems},
  journal = {Journal of Applied Logic},
  volume = 7,
  number = 1,
  pages = {41--57},
  year = 2009,
  note = "DOI: 10.1016/j.jal.2007.07.004"}

@inproceedings{blanchette-popescu-2013,
  author = "J. C. Blanchette and Andrei Popescu",
  title = "Mechanizing the Metatheory of {S}ledgehammer",
  editor = "P. Fontaine and C. Ringeissen and R. A. Schmidt",
  booktitle = {Frontiers of Combining Systems (FroCoS~2013\/)},
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  volume    = {8152},
  pages     = {245--260},
  year = 2013
}

@inproceedings{bobot-paskevich-2011,
  author = "Fran\c{c}ois Bobot and Andrei Paskevich",
  title = "Expressing Polymorphic Types in a Many-Sorted Language",
  editor    = {Cesare Tinelli and
               Viorica Sofronie-Stokkermans},
  booktitle = {Frontiers of Combining Systems (FroCoS~2011\/)},
  series = "Lecture Notes in Computer Science",
  volume    = {6989},
  publisher = "Springer",
  pages     = {87--102},
  year = 2011}

@inproceedings{boehme-nipkow-2010,
  title = "Sledgehammer: {J}udgement {D}ay",
  author = {Sascha B\"ohme and Tobias Nipkow},
  booktitle = {International Joint Conference on Automated Reasoning (IJCAR~2010\/)},
  editor = {J\"urgen Giesl and Reiner H\"ahnle},
  publisher="Springer",
  series={{Lecture Notes in Computer Science}},
  volume = 6173,
  pages = "107--121",
  year = 2010,
  note = "DOI: 10.1007/978-3-642-14203-1\_9"}

@inproceedings{hurd-2003,
  author = "Joe Hurd",
  title = "First-Order Proof Tactics in Higher-Order Logic Theorem Provers",
  editor = "Myla Archer and Ben {Di~Vito} and C{\'{e}}sar Mu{\~{n}}oz",
  booktitle = "Design and Application of Strategies/\kern.5pt Tactics in Higher Order Logics",
  xxxnumber = "CP-2003-212448",
  series = "{NASA} Tech.\ Reports",
  pages = "56--68",
  year = 2003}

@article{brand-1975,
  title = "Proving Theorems with the Modifiction Method",
  author = "D. Brand",
  journal = "SIAM J. Comput.",
  volume = 4,
  number = 4,
  year = 1975,
  pages = "412--430"
}

@article{bachmair-et-al-1995,
  author = "Leo Bachmair and Harald Ganzinger and Christopher Lynch and Wayne Snyder",
  title = "Basic Paramodulation",
  journal   = {Inf.\ Comput.},
  volume = 121,
  number = 2,
  year = 1995,
  pages = "172--192"
}

@misc{our-development,
  author = "J. C. Blanchette and Andrei Popescu",
  title = "Formal development associated with this paper",
  howpublished = "\href{http://www21.in.tum.de/~blanchet/fol_devel.tar.gz}
{\nolinkurl{www21.in.tum.de/~blanchet/fol_devel.tar.gz}}",
  year = 2012
}

@techreport{mccune-1994,
  author = "William McCune",
  title = "A {D}avis--{P}utnam Program and Its Application to Finite First-Order Model Search: Quasigroup Existence Problems",
  institution = "Argonne National Laboratory",
  year = 1994}

@inproceedings{korovin-2009,
  title = "Instantiation-Based Automated Reasoning: From Theory to Practice",
  author = "Konstantin Korovin",
  editor = "Renate A. Schmidt",
  booktitle = {CADE 2009},
  series = "Lecture Notes in Computer Science",
  volume = {5663},
  pages = "163--166",
  year = 2009,
  publisher = "Springer"}

@inproceedings{wenzel-1997,
  author = {Markus Wenzel},
  booktitle = {TPHOLs 1997},
  editor = {Elsa L. Gunter and Amy Felty},
  title = {Type Classes and Overloading in Higher-Order Logic},
  pages = {307--322},
  series = {{Lecture Notes in Computer Science}},
  volume = {1275},
  publisher = "Springer",
  year = {1997}}

@inproceedings{bouillaguet-et-al-2007,
  author    = {Charles Bouillaguet and
               Viktor Kuncak and
               Thomas Wies and
               Karen Zee and
               Martin C. Rinard},
  title     = {Using First-Order Theorem Provers in the {Jahob} Data Structure
               Verification System},
  booktitle = {VMCAI 2007},
  year      = {2007},
  pages     = {74--88},
  editor    = {Byron Cook and
               Andreas Podelski},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4349}
}
%Verification, Model Checking, and Abstract Interpretation

@inproceedings{margetson-ridge-2004,
  title = "Completeness Theorem",
  author = "James Margetson and Tom Ridge",
  booktitle = "Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher = "\href{http://afp.sf.net/entries/Completeness.shtml}
{\nolinkurl{afp.sf.net/entries/Completeness.shtml}}",
  year = 2004}

@inproceedings{klein-nipkow-2005,
  author    = {Gerwin Klein and
               Tobias Nipkow},
  title     = {Jinja is not {J}ava},
  booktitle   = {Archive of Formal Proofs},
  year      = {2005},
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher        = {\href{http://afp.sf.net/entries/Jinja.shtml}
{\nolinkurl{afp.sf.net/entries/Jinja.shtml}}}
}

@inproceedings{jiang-nipkow-2010,
  title = "Hall's Marriage Theorem",
  author = "Dongchen Jiang and Tobias Nipkow",
  booktitle = "Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher = "\href{http://afp.sf.net/entries/Marriage.shtml}
{\nolinkurl{afp.sf.net/entries/Marriage.shtml}}",
  year = 2010}

@inproceedings{harrison-2006,
  title = "Towards Self-Verification of {HOL Light}",
  author          = "John Harrison",
  editor          = "Ulrich Furbach and Natarajan Shankar",
  booktitle       = "International Joint Conference on Automated Reasoning (IJCAR 2006)",
  year            = 2006,
  publisher       = "Springer",
  series          = "Lecture Notes in Computer Science",
  volume          = 4130,
  pages           = "177--191"}


@inproceedings{mikhajlova-von-wright-1998,
  author = {Anna Mikhajlova and Joakim von Wright},
  title     = {Proving Isomorphism of First-Order Logic Proof Systems in {HOL}},
  booktitle = {TPHOLs},
  pages     = {295--314},
  editor    = {Jim Grundy and
               Malcolm C. Newey},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1479},
  year      = {1998}
}

@inproceedings{ridge-margetson-2005,
  author = {Tom Ridge and James Margetson},
  title     = {A Mechanically Verified, Sound and Complete Theorem Prover
               for First Order Logic},
  booktitle = {TPHOLs},
  year      = {2005},
  pages     = {294--309},
  editor = {Joe Hurd and Thomas F. Melham},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3603}
}

@book{shankar-1994,
  title = "Metamathematics, Machines, and Goedel's Proof",
  author = "Natarajan Shankar",
  series = "Cambridge Tracts in Theoretical Computer Science",
  volume = 38,
  publisher = "Cambridge University Press",
  year = 1994}

%%% todo: double-check, including J (and should be book chapter)
@inproceedings{mccune-shumski-2000,
  author = "William McCune and Olga Shumsky",
  title = "{Ivy}: A preprocessor and proof checker for first-order logic",
  editor = "M. Kaufmann and P. Manolios and {Strother~Moore, J}",
  booktitle = "Computer-Aided Reasoning: {ACL2} Case Studies",
  pages = "265--281",
  publisher = "Kluwer",
  year = 2000}

@inproceedings{claessen-sorensson-2003,
  title = { New Techniques that Improve {MACE}-Style Model Finding },
  author = { Koen Claessen and Niklas S{\"o}rensson },
  booktitle = { MODEL },
  year = { 2003 }
}

@inproceedings{paulson-blanchette-2010,
  author = "Lawrence C. Paulson and J. C. Blanchette",
  title = "Three Years of Experience with {Sledgehammer}, a~Practical Link Between Automatic and Interactive Theorem Provers",
  booktitle = "{International Workshop on the Implementation of Logics (IWIL-2010)}",
  editor    = {Geoff Sutcliffe and Stephan Schulz and Eugenia Ternovska},
  series    = {EPiC},
  volume    = {2},
  pages     = {1--11},
  year      = {2012},
  publisher = {EasyChair},
  note = "DOI: 10.29007/36dt"
}

%% cheat: incollection gives a , instead of a .
@inproceedings{wenzel-2007,
  author = 	 {Makarius Wenzel},
  title = 	 {{Isabelle/Isar}---{A} generic framework for human-readable proof documents},
  booktitle = 	 {From Insight to Proof---Festschrift in Honour of Andrzej Trybulec},
  publisher =	 {Uniwersytet w Bia{\l}ym\-stoku},
  year =	 2007,
  editor =	 {Roman Matuszewski and Anna Zalewska},
  volume =	 {10(23)},
  series =	 {Studies in Logic, Grammar, and Rhetoric}
}

@book{klein-et-al-afp,
  title = "Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher = "\href{http://afp.sf.net/}
{\nolinkurl{afp.sf.net}}"}

@inproceedings{margetson-ridge-2004,
  title = "Completeness Theorem",
  author = "James Margetson and Tom Ridge",
  booktitle = "Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher = "\href{http://afp.sf.net/entries/Completeness.shtml}
{\nolinkurl{afp.sf.net/entries/Completeness.shtml}}",
  year = 2004}

@inproceedings{popescu-traytel-2012-cards,
  title = "Ordinals and Cardinals in {HOL}",
  author = "Andrei Popescu and Dmitriy Traytel",
  publisher = "\href{http://www21.in.tum.de/~traytel/lics12_card.tgz}
{\nolinkurl{www21.in.tum.de/~traytel/lics12_card.tgz}}",
  year = 2012
}

@inproceedings{popescu-gunter-2011,
  author = {Andrei Popescu and Elsa L. Gunter},
  title     = {Recursion principles for syntax with bindings and substitution},
  booktitle = {ICFP 2011},
  year      = {2011},
  pages     = {346--358},
  editor    = {Manuel M. T. Chakravarty and
               Zhenjiang Hu and
               Olivier Danvy},
  publisher = {ACM}
}

@inproceedings{kammueller-et-al-1999,
  author    = {Florian Kamm{\"u}ller and
               Markus Wenzel and
               Lawrence C. Paulson},
  title     = {Locales---{A} Sectioning Concept for {I}sabelle},
  booktitle = {TPHOLs '99},
  year      = {1999},
  pages     = {149--166},
  editor    = {Yves Bertot and
               Gilles Dowek and
               Andr{\'e} Hirschowitz and
               C. Paulin and
               Laurent Th{\'e}ry},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1690}
}

@article{goguen-burstall-1992,
  author = {Joseph A. Goguen and Rod M. Burstall},
  title     = {Institutions: Abstract Model Theory for Specification and
               Programming},
  journal   = {J. ACM},
  volume    = {39},
  number    = {1},
  year      = {1992},
  pages     = {95--146}
}

@article{pitts-2003,
  author    = {Andrew M. Pitts},
  title     = {Nominal logic, a first order theory of names and binding},
  journal   = {Inf. Comput.},
  volume    = {186},
  number    = {2},
  year      = {2003},
  pages     = {165--193}
}

@inproceedings{pfenning-elliott-1988,
  author = {Frank Pfenning and Conal Elliott},
  title     = {Higher-Order Abstract Syntax},
  booktitle = {PLDI '88},
  year      = {1988},
  pages     = {199--208},
  editor    = {Richard L. Wexelblat},
  publisher = {ACM}
}

@inproceedings{blanchette-et-al-2012-spass,
  author = "J. C. Blanchette and Andrei Popescu and Daniel Wand and Christoph Weidenbach",
  title = "More {SPASS} with {Isabelle}: \allowbreak{S}uper\-po\-si\-tion with hard sorts and configurable~simplification",
  series = "Lecture Notes in Computer Science",
  year = 2012,
  editor = "Lennart Beringer and Amy Felty",
  booktitle = "Interactive Theorem Proving (ITP~2012\/)",
  volume = 7406,
  pages = "345--360",
  publisher = "Springer"}

@phdthesis{blanchette-2012-phd,
  author = "J. C. Blanchette",
  title = "Automatic Proofs and Refutations for Higher-Order Logic",
  school = {C.S.\ Department, Technische Universit\"at M\"unchen},
  type = "{Ph.D.}\ thesis",
  year = 2012}

@phdthesis{blanchette-2008-msc,
  author = "J. C. Blanchette",
  title = "Verification of Assertions in {C}reol Programs",
  school = {C.S.\ Department, Universitetet i Oslo},
  type = "{M.Sc.}\ thesis",
  year = 2008}

@misc{mml,
  key = "Aaa, Mizar Mathematical Library",
  title = "The {M}izar {M}athematical {L}ibrary",
  howpublished = "\href{http://mizar.org/}
{\nolinkurl{mizar.org}}"
}

@inproceedings{urban-2007,
  author    = {Josef Urban},
  title     = {{MaLARea}: A Metasystem for Automated Reasoning in Large Theories},
  booktitle = {ESARLT 2007},
  editor    = {Geoff Sutcliffe and
               Josef Urban and
               Stephan Schulz},
  publisher = {CEUR-WS.org},
  series    = {CEUR Workshop Proceedings},
  volume    = {257},
  year      = {2007}
}

@inproceedings{urban-et-al-2008,
  author = "Josef Urban and Geoff Sutcliffe and Petr Pudl{\'a}k and Ji\v{r}{\'\i} Vysko\v{c}il",
  title = "{MaLARea} {SG1}\dash {M}achine Learner for Automated Reasoning with Semantic Guidance",
  editor = "Alessandro Armando and Peter Baumgartner and Gilles Dowek",
  booktitle = "International Joint Conference on Automated Reasoning (IJCAR 2008)",
  volume = 5195,
  series = "Lecture Notes in Computer Science",
  pages = "441--456",
  publisher = "Springer",
  year = 2008}


@inproceedings{UrbanV13,
  author    = {Josef Urban and
               Ji\v{r}\'{\i} Vysko\v{c}il},
  title     = {Theorem Proving in Large Formal Mathematics as an Emerging
               {AI} Field},
  booktitle = {Automated Reasoning and Mathematics---Essays in Memory of William McCune},
  year      = {2013},
  pages = "240--257",
  crossref  = {2013bonacina}
}
%  note      = {to appear, \href{http://arxiv.org/abs/1209.3914}
{\nolinkurl{arxiv.org/abs/1209.3914}}},

@proceedings{2013bonacina,
  editor    = {Maria Paola Bonacina and
               Mark E. Stickel},
  title     = {Automated Reasoning and Mathematics---{E}ssays in Memory of William McCune},
  booktitle     = {Automated Reasoning and Mathematics---{E}ssays in Memory of William McCune},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7788},
  year      = {2013}
}
%  note = {to appear}

@inproceedings{Urban11-ate,
  author    = {Josef Urban},
  title     = {An Overview of Methods for Large-Theory Automated Theorem Proving},
  booktitle = {ATE-2011},
  year      = {2011},
  pages     = {3--8},
  crossref  = {ATE2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{ATE2011,
  editor    = {Peter H\"{o}fner and Annabelle McIver and
               Georg Struth},
  title     = {Proceedings of the First Workshop on Automated Theory Engineering},
  booktitle = {ATE-2011},
  publisher = {CEUR-WS.org},
  series    = {CEUR Workshop Proceedings},
  volume    = {760},
  year      = {2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{kaliszyk-urban-2013,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {Learning-assisted Automated Reasoning with {F}lyspeck},
  journal   = {CoRR},
  volume    = {abs/1211.7012},
  year      = {2012},
  note      = {\href{http://arxiv.org/abs/1211.7012}
{\nolinkurl{arxiv.org/abs/1211.7012}}}
}

@inproceedings{kuehlwein-et-al-2012-ijcar,
  author    = {Daniel K{\"u}hlwein and
               van Laarhoven, Twan and
               Evgeni Tsivtsivadze and
               Josef Urban and
               Tom Heskes},
  title     = {Overview and Evaluation of Premise Selection Techniques
               for Large Theory Mathematics},
  booktitle = {International Joint Conference on Automated Reasoning ({IJCAR}~2012\/)},
  editor    = {Bernhard Gramlich and
               Dale Miller and
               Uli Sattler},
  pages = "378--392",
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7364},
  year      = {2012}
}

@inproceedings{kuehlwein-urban-2012-paar,
  title={Learning from Multiple Proofs: First Experiments},
  author={Daniel K{\"u}hlwein and 
	  Josef Urban},
	editor="Pascal Fontaine and Renate Schmidt and Stephan Schulz",
  booktitle={PAAR-2012},
  pages={82--94},
  year      = {2012}
}

@inproceedings{alama-et-al-2012,
  author    = {Jesse Alama and
               Daniel K{\"u}hlwein and
               Josef Urban},
  title     = {Automated and Human Proofs in General Mathematics: An Initial
               Comparison},
  booktitle = {LPAR-18},
  year      = {2012},
  pages     = {37--45},
  editor    = {Nikolaj Bj{\o}rner and
               Andrei Voronkov},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7180},
}

@inproceedings{wenzel-2009,
  author = "Makarius Wenzel",
  title = "Parallel Proof Checking in {I}sabelle/{I}sar",
  editor = "Gabriel Dos{~}Reis and Laurent Th{\'e}ry",
  booktitle = "PLMMS 2009",
  pages = "13--29",
  publisher = "ACM Digital Library",
  year = 2009}

@article{Urban06-ijait,
  author =	 {Josef Urban},
  title =	 {{M}o{M}{M}---{F}ast Interreduction and Retrieval in
                  Large Libraries of Formalized Mathematics},
  journal =	 {Int.\ J. AI Tools},
  volume =	 {15},
  number =	 {1},
  year =	 {2006},
  pages =	 {109--130}
}


@article{UrbanRS13,
year={2013},
issn={0168-7433},
journal={J.~Automated Reasoning},
volume={50},
number={2},
title={{ATP} and Presentation Service for {M}izar Formalizations},
publisher={Springer Netherlands},
author={Urban, Josef and Rudnicki, Piotr and Sutcliffe, Geoff},
pages={229--241},
}

@article{sultana-et-al-2013,
  author = {Nik Sultana and J. C. Blanchette and Lawrence C. Paulson},
  title = "{LEO-II} and {Satallax} on the {Sledgehammer} Test Bench",
  journal = {Journal of Applied Logic},
  volume = 11,
  number = 1,
  pages = {91--102},
  year = 2013}

@inproceedings{berghofer-nipkow-2000,
  author    = {Stefan Berghofer and
               Tobias Nipkow},
  title     = {Proof Terms for Simply Typed Higher Order Logic},
  booktitle = {TPHOLs 2000},
  pages     = {38--52},
  editor    = {Mark Aagaard and
               John Harrison},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1869},
  year      = {2000}
}

@article{paulson-1998,
  author    = {Lawrence C. Paulson},
  title     = {The Inductive Approach to Verifying Cryptographic Protocols},
  journal   = {J. Comput.\ Secur.},
  volume    = {6},
  number    = {1--2},
  year      = {1998},
  pages     = {85--128}
}

@article{sutcliffe-2009-lib,
  author = "Geoff Sutcliffe",
  title = "The {TPTP} Problem Library and Associated Infrastructure---{T}he {FOF} and {CNF} Parts, v3.5.0",
  journal = "Journal of Automated Reasoning",
  volume = "43",
  number = 4,
  pages = "337--362",
  year = 2009}

@inproceedings{benzmueller-et-al-2008-leo2,
  author = "Christoph Benzm{\"u}ller and Lawrence C. Paulson and Frank Theiss and Arnaud Fietzke",
  title = "{LEO-II}---{A} Cooperative Automatic Theorem Prover for Higher-Order Logic",
  editor = "Alessandro Armando and Peter Baumgartner and Gilles Dowek",
  booktitle = "International Joint Conference on Automated Reasoning (IJCAR 2008)",
  publisher="Springer",
  series={{Lecture Notes in Computer Science}},
  volume = 5195,
  pages = "162--170",
  year = 2008}

@inproceedings{brown-2012-ijcar,
  author    = {Chad E. Brown},
  title     = {{S}atallax: {A}n Automatic Higher-Order Prover},
  booktitle = {International Joint Conference on Automated Reasoning ({IJCAR}~2012\/)},
  editor    = {Bernhard Gramlich and
               Dale Miller and
               Uli Sattler},
  pages = "111--117",
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7364},
  year      = {2012}
}

@inproceedings{barrett-tinelli-2007,
  author    = {Clark Barrett and Cesare Tinelli},
  title     = {{CVC3}},
  booktitle = {Computer Aided Verification (CAV 2007\/)},
  editor    = {Werner Damm and Holger Hermanns},
  volume    = {4590},
  series    = "Lecture Notes in Computer Science",
  pages     = {298--302},
  publisher = {Springer},
  year      = {2007}
}

@misc{dutertre-de-moura-2006-yices,
  author    = {Bruno Dutertre and de Moura, Leonardo},
  title     = {The {Yices} {SMT} Solver},
  howpublished = "\href{http://yices.csl.sri.com/tool-paper.pdf}
{\nolinkurl{yices.csl.sri.com/tool-paper.pdf}}",
  year = 2006}

@article{blistr,
  author    = {Josef Urban},
  title     = {{BliStr}: The Blind Strategymaker},
  journal   = {CoRR},
  volume    = {abs/1301.2683},
  year      = {2013},
  note        = {\href{http://arxiv.org/abs/1301.2683}
{\nolinkurl{arxiv.org/abs/1301.2683}}}
}

@inproceedings{hoder-2011,
  author = "Kry\v{s}tof Hoder and Andrei Voronkov",
  title = "Sine Qua Non for Large Theory Reasoning",
  editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
  booktitle = {CADE 2011},
  year = 2011,
  series = "Lecture Notes in Computer Science",
  volume = "6803",
  pages = " 299--314",
  publisher = "Springer"}

@misc{schulz-2011-ringberg,
  author = "Stephan Schulz",
  title = "First-Order Deduction for Large Knowledge Bases",
  howpublished = "Presentation at Deduction at Scale 2011 Seminar, Ringberg Castle",
  year = 2011,
  url = "http://www.mpi-inf.mpg.de/departments/rg1/conferences/deduction10/slides/stephan-schulz.pdf"
}
% http://www.mpi-inf.mpg.de/departments/rg1/conferences/deduction10/slides/stephan-schulz.pdf

@misc{kolanski-2011,
  author = "Rafal Kolanski",
  month = "January",
  year = 2011,
  howpublished = "Private communication"}

@misc{paulson-2012,
  author = "Lawrence C. Paulson",
  month = "April",
  year = "2012",
  howpublished = "Private communication"}

@article{gonthier-2008,
  title = "Formal Proof---{T}he Four-Color Theorem",
  author = "Georges Gonthier",
  journal = "Notices of the AMS",
  volume = 55,
  number = 11,
  pages = "1382--1393",
  year = 2008}
%journal = "Notices AMS",

@article{leroy-2009-jar,
  author    = {Xavier Leroy},
  title     = {A Formally Verified Compiler Back-end},
  journal   = {J.~Automated Reasoning},
  volume    = {43},
  number    = {4},
  year      = {2009},
  pages     = {363--446}
}

@article{klein-et-al-2010,
  author    = {Gerwin Klein and
               June Andronick and
               Kevin Elphinstone and
               Gernot Heiser 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 operating-system kernel},
  journal   = {Communications of the ACM},
  volume    = {53},
  number    = {6},
  year      = {2010},
  pages     = {107--115}
}

@inproceedings{hales-2013,
  author = "Thomas C. Hales",
  title = "External Tools for the Formal Proof of the {Kepler} Conjecture",
  editor = "J. C. Blanchette and Josef Urban",
  booktitle = "PxTP~2013",
  pages = "1",
  series    = {EPiC},
  volume    = {14},
  publisher = {EasyChair},
  year = 2013}

@inproceedings{blanchette-2013,
  author = "J. C. Blanchette",
  title = "Redirecting Proofs by Contradiction",
  editor = "J. C. Blanchette and Josef Urban",
  booktitle = "PxTP~2013",
  pages = "11--26",
  series    = {EPiC},
  volume    = {14},
  publisher = {EasyChair},
  year = 2013}

@proceedings{blanchette-urban-2013,
  editor = "J. C. Blanchette and Josef Urban",
  title = "PxTP~2013",
  series    = {EPiC},
  volume    = {14},
  publisher = {EasyChair},
  year = 2013}

@inproceedings{smolka-blanchette-2013,
  author = "Steffen Juilf Smolka and J. C. Blanchette",
  title = "Robust, Semi-Intelligible {I}sabelle Proofs from {ATP} Proofs",
  editor = "J. C. Blanchette and Josef Urban",
  booktitle = "PxTP~2013",
  pages = "117--132",
  series    = {EPiC},
  volume    = {14},
  publisher = {EasyChair},
  year = 2013}

@inproceedings{rudnicki-urban-2011,
  author = "Piotr Rudnicki and Josef Urban",
  title = "Escape to {ATP} for {M}izar",
  editor = "Pascal Fontaine and Aaron Stump",
  booktitle = "PxTP 2011",
  year = 2011}


@inproceedings{kuehlwein-et-al-2013-mash,
  title = "{MaSh}: Machine learning for {S}ledgehammer",
  author = {Daniel K\"uhlwein and J. C. Blanchette and Cezary Kaliszyk
   and Josef Urban},
  pages = "35--50",
  crossref = "itp2013"}

@article{blanchette-2013-relational,
  title = "Relational Analysis of (Co)inductive Predicates, (Co)inductive Data\-types, and (Co)recursive Functions",
  author = "J. C. Blanchette",
  journal = {Softw.\ Qual.\ J.},
  volume = 21,
  number = 1,
  pages = {101--126},
  year = 2013}

@inproceedings{blanchette-et-al-2011-cpp,
  author = "J. C. Blanchette and Tjark Weber and Mark Batty and Scott Owens and Susmit Sarkar",
  title = "Nitpicking \cpp{} concurrency",
  booktitle = "PPDP 2011",
  pages = "113--124",
  publisher = "ACM~Press",
  year = 2011}

@unpublished{blanchette-et-al-2013-compl,
  author = "J. C. Blanchette and Andrei Popescu and Dmitriy Traytel",
  title = "Coinductive pearl: Modular first-order logic completeness",
  note = "Submitted"}

@incollection{traytel-et-al-2012,
  author = "Dmitriy Traytel and Andrei Popescu and J. C. Blanchette",
  title     = {Foundational, Compositional (Co)datatypes for Higher-Order
               Logic---{C}ategory Theory Applied to Theorem Proving},
  year      = {2012},
  pages     = {596--605},
  booktitle = {Logic in Computer Science (LICS 2012\/)},
  publisher = {{IEEE} Computer Society}
}

@inproceedings{guttmann-et-al-2011,
  author = {Walter Guttmann and Georg Struth and Tjark Weber},
  title  = {Automating Algebraic Methods in {Isabelle}},
  booktitle = {ICFEM 2011},
  editor = "Qin, Shengchao and Qiu, Zongyan",
  year   = {2011},
  series = "Lecture Notes in Computer Science",
  volume  = "6991",
  pages = "617--632",
  publisher = "Springer"
}

@article{blanchette-2009-huffman,
  title = "Proof pearl: Mechanizing the textbook proof of {H}uffman's algorithm in {Isabelle\slash HOL}",
  author = "J. C. Blanchette",
  journal = {;;;;;;;;$1omated Reasoning},
  volume = {43},
  number = {1},
  pages = {1--18},
  year = 2009}

@inproceedings{blanchette-nipkow-2009,
  title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (Extended Abstract)",
  author = "J. C. Blanchette and Tobias Nipkow",
  editor = "Catherine Dubois",
  booktitle = "Tests and Proofs (TAP 2009): Short Papers",
  series = "{ETH} Tech.\ Reports",
  year = 2009}

@inproceedings{blanchette-2010-relational,
  title = "Relational Analysis of (Co)inductive Predicates, (Co)inductive Datatypes, and (Co)recursive Functions",
  author = "J. C. Blanchette",
  booktitle = "TAP~2010",
  editor = "Gordon Fraser and Angelo Gargantini",
  publisher="Springer",
  series = {{Lecture Notes in Computer Science}},
  volume = "6143",
  pages = "117--134",
  year = 2010}

@inproceedings{blanchette-krauss-2010,
  title = "Monotonicity Inference for Higher-Order Formulas",
  author = "J. C. Blanchette and Alexander Krauss",
  booktitle = "International Joint Conference on Automated Reasoning (IJCAR~2010)",
  editor = {J\"urgen Giesl and Reiner H\"ahnle},
  publisher="Springer",
  series={{Lecture Notes in Computer Science}},
  volume = 6173,
  pages = "91--106",
  year = 2010}

@inproceedings{blanchette-claessen-2010,
  title = "Generating counterexamples for structural inductions by exploiting
nonstandard~models",
  author = "J. C. Blanchette and Koen Claessen",
  editor = "Christian G. Ferm{\"u}ller and Andrei Voronkov",
  booktitle = "LPAR-17",
  year      = {2010},
  pages     = {117--141},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume = 6397}

@inproceedings{blanchette-et-al-2011-smt,
  author = {J. C. Blanchette and Sascha B{\"o}hme and  Lawrence C. Paulson},
  title = "Extending {S}ledgehammer with {SMT} Solvers",
  editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
  booktitle = {CADE-23},
  year = 2011,
  series = "Lecture Notes in Computer Science",
  volume = "6803",
  pages = "207--221",
  publisher = "Springer"}

@inproceedings{blanchette-et-al-2011-frocos,
  author = "J. C. Blanchette and Lukas Bulwahn and Tobias Nipkow",
  title = "Automatic Proof and Disproof in {Isabelle\slash HOL}",
  editor = "Cesare Tinelli and Viorica Sofronie-Stokkermans",
  booktitle = {Frontiers of Combining Systems (FroCoS~2011\/)},
  series = "Lecture Notes in Computer Science",
  volume = 6989,
  publisher = "Springer",
  pages = "12--27",
  year = 2011}

@inproceedings{blanchette-2010-nitpick,
  author    = {J. C. Blanchette},
  title     = {Nitpick: A Counterexample Generator for {Isabelle/HOL} Based on the Relational Model Finder {K}odkod (system description)},
  booktitle = {Logic for Programming, Artificial Intelligence and Reasoning (LPAR-17) Short Papers},
  editor    = {Andrei Voronkov and Geoff Sutcliffe and Matthias Baaz and Christian Ferm\"uller},
  series    = {EPiC},
  volume    = {13},
  pages     = {20--25},
  year      = {2013},
  publisher = {EasyChair}
}

@article{blanchette-owe-2008,
  title = "An open system operational semantics for an object-oriented and component-based~language",
  author = "J. C. Blanchette and Olaf Owe",
  journal   = {Electr.\ Notes Theor.\ Comput.\ Sci.},
  volume    = {215},
  year      = {2008},
  pages     = {151--169}
}

@article{johnsen-et-al-2009,
  title = "Intra-Object versus Inter-Object: Concurrency and Reasoning in {C}reol",
  author = "Einar Broch Johnsen and J. C. Blanchette and Marcel Kyas and Olaf Owe",
  journal   = {Electr.\ Notes Theor.\ Comput.\ Sci.},
  volume    = {243},
  year      = {2009},
  pages     = {89--103}
}

@inproceedings{blanchette-2008-afp,
  title = "The Textbook Proof of {H}uffman's Algorithm",
  author = "J. C. Blanchette",
  booktitle = "Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher = "\href{http://afp.sf.net/entries/Huffman.shtml}
{\nolinkurl{afp.sf.net/entries/Huffman.shtml}}",
  year = 2008}

@inproceedings{blanchette-popescu-2013-afp,
  title = "Sound and Complete Sort Encodings for First-Order Logic",
  author = "J. C. Blanchette and Andrei Popescu",
  booktitle = "Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher = "\href{http://afp.sf.net/entries/Sort_Encodings.shtml}
{\nolinkurl{afp.sf.net/entries/Sort_Encodings.shtml}}",
  year = 2013}

@book{blanchette-summerfield-2004,
  author    = {J. Blanchette and Mark Summerfield},
  title     = {\cpp{} GUI Programming with Qt 3},
  publisher = "Bruce Perens' Open Source Series, Prentice~Hall",
  year      = {2004}
}

@book{blanchette-summerfield-2006,
  author    = {J. Blanchette and Mark Summerfield},
  title     = {\cpp{} GUI Programming with Qt 4},
  publisher = "Prentice~Hall",
  year      = {2006}
}

@book{blanchette-summerfield-2008,
  author    = {J. Blanchette and Mark Summerfield},
  title     = {\cpp{} GUI Programming with Qt 4, Second Edition},
  publisher = {Open Source Software Development Series, Prentice~Hall},
  year      = {2008}
}

@book{blanchette-2008-api,
  author = "J. Blanchette",
  title = "The Little Manual of {API} Design",
  publisher = "Trolltech, a Nokia company, \href{http://www21.in.tum.de/~blanchet/api-design.pdf}
{\nolinkurl{www21.in.tum.de/~blanchet/api-design.pdf}}",
  year = 2008}

@book{jackson-2006,
  author = "Daniel Jackson",
  title = "Software Abstractions: Logic, Language, and Analysis",
  publisher = "MIT~Press",
  year = 2006}

@techreport{leino-moskal-201x,
  author = {K. Rustan M. Leino and Micha{\l} Moskal},
  title = {Co-induction Simply},
  year = {2013},
  institution = {Microsoft Research},
  xxxnumber = {MSR-TR-2013-49},
  note = "\href{http://research.microsoft.com/pubs/192276/coinduction.pdf}
{\nolinkurl{research.microsoft.com/pubs/192276/coinduction.pdf}}",
}

%%% TODO: check URL
@misc{blanchette-et-al-2013-manual,
  title = "Defining (Co)datatypes in {I}sabelle/{HOL}",
  author = "J. C. Blanchette and Lorenz Panny and Andrei Popescu and Dmitriy Traytel",
  howpublished = "\href{http://isabelle.in.tum.de/dist/Isabelle/doc/datatypes.pdf}
{\nolinkurl{isabelle.in.tum.de/dist/Isabelle/doc/datatypes.pdf}}",
  year = 2013}

@inproceedings{kaliszyk-krauss-2013,
  author    = {Cezary Kaliszyk and Alexander Krauss},
  title     = {Scalable {LCF}-Style Proof Translation},
  pages     = {51--66},
  crossref = "itp2013"}

@inproceedings{aydemir-et-al-2005,
  author    = {Brian E. Aydemir and
               Aaron Bohannon and
               Matthew Fairbairn and
               J. Nathan Foster and
               Benjamin C. Pierce and
               Peter Sewell and
               Dimitrios Vytiniotis and
               Geoffrey Washburn and
               Stephanie Weirich and
               Steve Zdancewic},
  title     = {Mechanized Metatheory for the Masses: The \textsc{PoplMark} Challenge},
  booktitle = {TPHOLs 2005},
  pages     = {50--65},
  editor    = {Joe Hurd and
               Thomas F. Melham},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3603},
  year      = {2005}
}

@inproceedings{esparza-et-al-2013,
  author    = {Javier Esparza and
               Peter Lammich and
               Ren{\'e} Neumann and
               Tobias Nipkow and
               Alexander Schimpf and
               Jan-Georg Smaus},
  title     = {A Fully Verified Executable {LTL} Model Checker},
  booktitle = {Computer Aided Verification (CAV 2013\/)},
  year      = {2013},
  pages     = {463--478},
  editor    = {Natasha Sharygina and
               Helmut Veith},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {8044}
}

@article{hoare-2003,
  author = {C.~A.~R. Hoare},
  title     = {The verifying compiler: A grand challenge for computing research},
  journal   = {J. ACM},
  volume    = {50},
  number    = {1},
  year      = {2003},
  pages     = {63--69}
}

@inproceedings{filliatre-paskevich-2013,
  author    = {Jean-Christophe Filli{\^a}tre and Andrei Paskevich},
  title     = {Why3---{W}here Programs Meet Provers},
  booktitle = {ESOP 2013},
  year      = {2013},
  pages     = {125--128},
  editor    = {Matthias Felleisen and
               Philippa Gardner},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7792}
}

@article{hales-et-al-2017,
    AUTHOR = {Hales, Thomas and Adams, Mark and Bauer, Gertrud and Dang, Tat
              Dat and Harrison, John and Le Truong Hoang and Kaliszyk,
              Cezary and Magron, Victor and McLaughlin, Sean and Nguyen, Tat
              Thang and Nguyen, Quang Truong and Nipkow, Tobias and Obua,
              Steven and Pleso, Joseph and Rute, Jason and Solovyev, Alexey
              and Ta, Thi Hoai An and Tran, Nam Trung and Trieu, Thi Diep
              and Urban, Josef and Vu, Ky and Zumkeller, Roland},
     TITLE = {A formal proof of the {K}epler conjecture},
  JOURNAL = {Forum of Mathematics, Pi},
    VOLUME = {5},
      YEAR = {2017},
     PAGES = {e2, 29},
      ISSN = {2050-5086},
   MRCLASS = {52C17 (05B40)},
  MRNUMBER = {3659768},
MRREVIEWER = {Martin\ Henk},
       DOI = {10.1017/fmp.2017.1},
       URL = {https://doi.org/10.1017/fmp.2017.1},
       note = "DOI: 10.1017/fmp.2017.1",
}
@proceedings{itp2013,
  editor = "S. Blazy and C. Paulin-Mohring and D. Pichardie",
  title = "Interactive Theorem Proving (ITP 2013\/)",
  booktitle = "Interactive Theorem Proving (ITP 2013\/)",
  series = "Lecture Notes in Computer Science",
  volume = 7998,
  publisher = "Springer",
  year = 2013}

@inproceedings{lochbihler-2010,
  author    = {Andreas Lochbihler},
  title     = {Verifying a Compiler for Java Threads},
  pages     = {427--447},
  crossref = "esop2010"
}

@proceedings{esop2010,
  editor    = {Andrew D. Gordon},
  title     = {{ESOP} 2010},
  series    = {Lecture Notes in Computer Science},
  volume    = {6012},
  publisher = {Springer},
  year      = {2010}
}

@inproceedings{de-gouw-et-al-2015,
  author    = {Stijn de Gouw and
               Jurriaan Rot and
               Frank S. de Boer and
               Richard Bubel and
               Reiner H{\"{a}}hnle},
  title     = {{OpenJDK}'s {Java.utils.Collection.sort()} Is Broken: The Good, the Bad
               and the Worst Case},
  pages     = {273--289},
  crossref  = {cav2015},
}

@proceedings{cav2015,
  editor    = {Daniel Kroening and
               Corina S. Pasareanu},
  title     = {{CAV} 2015},
  booktitle     = {{CAV} 2015},
  series    = {Lecture Notes in Computer Science},
  volume    = {9206},
  publisher = {Springer},
  year      = {2015}
}

@article{hales-2014-bourbaki,
  author    = {Thomas C. Hales},
  title     = {Developments in Formal Proofs},
  journal   = {CoRR},
  volume    = {abs/1408.6474},
  year      = {2014},
  url       = {http://arxiv.org/abs/1408.6474},
  timestamp = {Fri, 12 Sep 2014 12:44:21 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/Hales14},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  note      = {Séminaire Bourbaki, 66ème année, 2013--2014, n\textsuperscript{o} 1086.
    Available at \url{http://arxiv.org/abs/1408.6474}}}

@misc{paulson-2012-pc,
  author = "Lawrence C. Paulson",
  title = "Private communication",
  year = "Apr.\ 2012"}

@misc{nipkow-2013-pc,
  author = "Tobias Nipkow",
  title = "Private communication",
  year = "Sept.\ 2013"}

@misc{nipkow-2015-pc,
  author = "Tobias Nipkow",
  title = "Private communication",
  year = "June 2015"}

@misc{voronkov-2011-pc,
  author = "Andrei Voronkov",
  year = "Aug.\ 2011",
  howpublished = "Private communication"}

@inproceedings{bundy-2002,
  author    = {Alan Bundy},
  title     = {A Critique of Proof Planning},
  booktitle = {Computational Logic: Logic Programming and Beyond, Essays in Honour
               of Robert A. Kowalski{\upshape, part {II}}},
  pages     = {160--177},
  year      = {2002},
  crossref  = {kowalski2002-2}
}

@proceedings{kowalski2002-2,
  editor    = {Antonis C. Kakas and
               Fariba Sadri},
  title     = {Computational Logic: Logic Programming and Beyond, Essays in Honour
               of Robert A. Kowalski, Part {II}},
  series    = {Lecture Notes in Computer Science},
  volume    = {2408},
  publisher = {Springer},
  year      = {2002}
}

@misc{wand-weidenbach-201x,
  title = "Automatic Induction inside Superposition",
  author = "Daniel Wand and Christoph Weidenbach",
  note = "Unpublished draft. Available at \url{http://people.mpi-inf.mpg.de/~dwand/datasup/draft.pdf}"}

@phdthesis{cruanes-2015,
  author = "Simon Cruanes",
  title = "Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond",
  type = "{Ph.D.}\ thesis",
  school = "\'Ecole polytechnique",
  year = 2015,
  note = "Available at \url{https://who.rocq.inria.fr/Simon.Cruanes/files/thesis.pdf}"}

@inproceedings{reynolds-kuncak-2015,
  title = "Induction for {SMT} Solvers",
  author = "Andrew Reynolds and Viktor Kuncak",
  booktitle = {Verification, Model Checking and Abstract Interpretation ({VMCAI} 2014\/)},
  pages     = {80--98},
  editor    = {Deepak D'Souza and
               Akash Lal and
               Kim Guldstrand Larsen},
  series    = {Lecture Notes in Computer Science},
  volume    = {8931},
  publisher = {Springer},
  year      = {2014}
}

@inproceedings{gupta-et-al-2014,
  author    = {Ashutosh Gupta and
               Laura Kov{\'{a}}cs and
               Bernhard Kragl and
               Andrei Voronkov},
  title     = {Extensional Crisis and Proving Identity},
  pages     = {185--200},
  editor    = {Franck Cassez and
               Jean{-}Fran{\c{c}}ois Raskin},
  booktitle     = {Automated Technology for Verification and Analysis ({ATVA} 2014\/)},
  series    = {Lecture Notes in Computer Science},
  volume    = {8837},
  publisher = {Springer},
  year      = {2014}
}

@article{wolchover-2013,
  author = "Natalie Wolchover",
  title = "As Math Grows More Complex, Will Computers Reign?",
  journal = "Wired",
  dateXXX = "3 Apr.\ 2013",
  year = "2013",
  note = "Available at \url{http://www.wired.com/2013/03/computers-and-math/}"
}

@inproceedings{robinson-1968,
  author    = {John Alan Robinson},
  title     = {New directions in mechanical theorem proving},
  booktitle = {International Federation for Information Processing ({IFIP} 1968\/)},
  volume = 1,
  pages     = {63--69},
  year      = {1968},
  timestamp = {Thu, 03 Jan 2002 12:03:25 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/ifip/Robinson68},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{reynolds-blanchette-2015-codp,
  author    = {Andrew Reynolds and
               Jasmin Christian Blanchette},
  title     = {A Decision Procedure for (Co)datatypes in {SMT} Solvers},
  pages     = {197--213},
  editor    = {Amy P. Felty and
               Aart Middeldorp},
  booktitle = {Conference on Automated Deduction (CADE-25\/)},
  series    = {Lecture Notes in Computer Science},
  volume    = {9195},
  publisher = {Springer},
  year      = {2015},
}

@inproceedings{voronkov-2014,
  author    = {Andrei Voronkov},
  title     = {{AVATAR}: The Architecture for First-Order Theorem Provers},
  pages     = {696--710},
  crossref  = {cav2014}
}

@proceedings{cav2014,
  editor    = {Armin Biere and
               Roderick Bloem},
  booktitle = {Computer Aided Verification (CAV 2014\/)},
  series    = {Lecture Notes in Computer Science},
  volume    = {8559},
  publisher = {Springer},
  year      = {2014},
}

@inproceedings{ge-de-moura-2009,
  author    = {Yeting Ge and
               de Moura, Leonardo},
  title     = {Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo
               Theories},
  pages     = {306--320},
  year      = {2009},
  crossref  = {cav2009},
}

@proceedings{cav2009,
  editor    = {Ahmed Bouajjani and
               Oded Maler},
  title     = {{CAV} 2009},
  booktitle     = {{CAV} 2009},
  series    = {Lecture Notes in Computer Science},
  volume    = {5643},
  publisher = {Springer},
  year      = {2009},
}

@inproceedings{bouton-et-al-2009,
  author    = {Thomas Bouton and
               Diego Caminha B. de Oliveira and
               David D{\'e}harbe and
               Pascal Fontaine},
  title     = {{veriT}: An Open, Trustable and Efficient {SMT}-Solver},
  pages     = {151--156},
  editor    = {Renate A. Schmidt},
  booktitle = {Conference on Automated Deduction (CADE-22\/)},
  year      = {2009},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5663}
}

@book{stroustrup-1994,
  author = "Bjarne Stroustrup",
  title = "The Design and Evolution of C++",
  publisher = "Addison-Wesley",
  year = 1994}

@inproceedings{reynolds-et-al-2014-qi,
  author    = {Andrew Reynolds and
               Cesare Tinelli and
               de Moura, Leonardo},
  title     = {Finding conflicting instances of quantified formulas in {SMT}},
  pages     = {195--202},
  booktitle     = {Formal Methods in Computer-Aided Design ({FMCAD} 2014\/)},
  publisher = {{IEEE} Computer Society},
  year      = {2014}
}

@inproceedings{brown-2012,
  author    = {Chad E. Brown},
  title     = {Satallax: An Automatic Higher-Order Prover},
  pages     = {111--117},
  year      = {2012},
  editor    = {Bernhard Gramlich and
               Dale Miller and
               Uli Sattler},
  booktitle = {International Joint Conference on Automated Reasoning ({IJCAR}~2012\/)},
  series    = {Lecture Notes in Computer Science},
  volume    = {7364},
  publisher = {Springer},
}

@inproceedings{chaudhuri-et-al-2010,
  author    = {Kaustuv Chaudhuri and
               Damien Doligez and
               Leslie Lamport and
               Stephan Merz},
  title     = {The {\tlaplus} {P}roof {S}ystem: Building a Heterogeneous
               Verification Platform},
  booktitle = {International Colloquium on Theoretical Aspects of Computing (ICTAC 2010\/)},
  pages     = {44},
  editor    = {Ana Cavalcanti and
               David D{\'e}harbe and
               Marie-Claude Gaudel and
               Jim Woodcock},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6255},
  year      = {2010}
}

@book{bertot-casteran-2004,
  title = "Interactive Theorem Proving and Program Development: {Coq'Art}: The Calculus of Inductive Constructions",
  series = "Texts in Theoretical Computer Science",
  publisher = "Springer",
  author = "Bertot, Yves and Cast\'eran, Pierre",
  year = 2004,
  note = "DOI: 10.1007/978-3-662-07964-5"}

% March 2015
@article{newcombe-et-al-2015,
  author = "Chris Newcombe and Tim Rath and Fan Zhang and Bogdan Munteanu and Marc Brooker and Michael Deardeuff",
  year = 2015,
  title = "How {A}mazon {W}eb {S}ervices uses formal methods",
  journal = "Communications of the ACM",
  volume = 58,
  number = 4,
  pages = "66--73"}

@misc{blanchette-2015-coqws,
  title = "Toward {N}itpick and {S}ledgehammer for {C}oq",
  author = "Jasmin Christian Blanchette",
  year = 2014,
  note = "Presented at Coq 2015"}

@article{russinoff-1999,
  author    = {David M. Russinoff},
  title     = {A Mechanically Checked Proof of Correctness of the {AMD} {K5} Floating
               Point Square Root Microcode},
  journal   = {Formal Methods in System Design},
  volume    = {14},
  number    = {1},
  pages     = {75--125},
  year      = {1999}
}

@inproceedings{harrison-2003,
  author    = {John Harrison},
  title     = {Formal Verification at {I}ntel},
  booktitle = {Logic in Computer Science (LICS 2003\/)},
  pages     = {45--54},
  year      = {2003},
  publisher = {{IEEE} Computer Society}
}

% http://blogs.scientificamerican.com/guest-blog/voevodskye28099s-mathematical-revolution/

@misc{rehmeyer-2013,
  title = "{V}oevodsky's Mathematical Revolution",
  author = "Julie Rehmeyer",
  dateXXX = "1 Oct.\ 2013",
  howpublished = "\emph{Scientific American} Blogs",
  year = 2013,
  note = "Available at \url{http://blogs.scientificamerican.com/guest-blog/voevodskye28099s-mathematical-revolution/}"
}

@article{leroy-2009-cacm,
  author    = {Xavier Leroy},
  title     = {Formal verification of a realistic compiler},
  journal   = {Communications of the {ACM}},
  volume    = {52},
  number    = {7},
  pages     = {107--115},
  year      = {2009}
}

@inproceedings{batty-et-al-2011,
  title = "Mathematizing \cpp{} Concurrency",
  author = "Mark Batty and Scott Owens and Susmit Sarkar and Peter Sewell and Tjark Weber",
  booktitle = "Principles of Programming Languages (POPL 2011\/)",
  editor = "Thomas Ball and Mooly Sagiv",
  pages = {55--66},
  publisher = {ACM},
  year = 2011}


@inproceedings{pierce-2009,
  author    = {Benjamin C. Pierce},
  title     = {Lambda, the ultimate {TA}: Using a proof assistant to teach programming
               language foundations},
  booktitle = {International Conference on Functional Programming ({ICFP} 2009\/)},
  pages     = {121--122},
  year      = {2009},
  editor    = {Graham Hutton and
               Andrew P. Tolmach},
  publisher = {{ACM}},
}

@article{lochbihler-2014,
  author = "Andreas Lochbihler",
  title = "Making the {Java} Memory Model Safe",
  journal = "ACM Transactions on Programming Languages and Systems",
  volume = 35,
  number = 4,
  year = 2014,
  pages = "12:1--65",
} 

@article{paulson-2015,
  author    = {Lawrence C. Paulson},
  title     = {A Mechanised Proof of {G}{\"{o}}del's Incompleteness Theorems Using
               {N}ominal {I}sabelle},
  journal   = {J.~Automated Reasoning},
  volume    = {55},
  number    = {1},
  pages     = {1--37},
  year      = {2015}
}

@misc{nicta-2015,
  author = "NICTA",
  title = "https://ssrg.nicta.com.au/jobs/proof-engineers2015",
  note = "\url{https://ssrg.nicta.com.au/jobs/proof-engineers2015}"}

@inproceedings{moura-bjoerner-2007,
         title = {Efficient {E}-Matching for {SMT} Solvers},
        author = {de Moura, Leonardo and Nikolaj Bj{\o}rner},
        editor = {Frank Pfenning},
        booktitle = {Conference on Automated Deduction (CADE-21\/)},
          year = {2007},
         pages = {183--198},
     publisher = {Springer},
        series = {Lecture Notes in Computer Science},
        volume = {4603}
}

@inproceedings{wand-2014,
  title = "Polymorphic+Typeclass Superposition",
  author = "Daniel Wand",
  pages = "105-119",
  booktitle = "Workshop on Practical Aspects of Automated Reasoning (PAAR-2014\/)",
  editor = "Stephan Schulz and de Moura, Leonardo and Boris Konev",
  series    = {EPiC},
  volume    = {31},
  year      = {2014},
  publisher = {EasyChair}  
}

@book{kaufmann-et-al-2000,
 author = {Matt Kaufmann and {J~Strother~Moore} and Panagiotis Manolios},
 title = {Computer-Aided Reasoning: An Approach},
 year = {2000},
 publisher = {Kluwer Academic Publishers},
 note = "DOI: 10.1007/978-1-4615-4449-4"
 }

@misc{sel4-projects,
  author = "NICTA",
  title = "{seL4} Community Projects",
  note = "\url{http://sel4.systems/Community/Projects/}"}

@misc{blazy-compcert,
  author = "Sandrine Blazy",
  title = "Compiling avionics software with the {CompCert} formally verified compiler",
  howpublished = "Dagstuhl seminar on Qualification of Formal Methods Tools",
  year = 2015,
  note = "Available
    at \url{http://materials.dagstuhl.de/files/15/15182/15182.SandrineBlazy.Slides.pdf}"}

@article{blanchette-et-al-2016-mash,
  title = "A learning-based fact selector for {I}sabelle/{HOL}",
  author = {J. C. Blanchette and David Greenaway and Cezary Kaliszyk and Daniel K\"uhlwein
   and Josef Urban},
  journal = "Journal of Automated Reasoning",
  volume = "57",
  number = "3",
  pages = "219--244",
  year = 2016,
  note = "DOI: 10.1007/s10817-016-9362-8"}

@misc{mccune-2003,
    Author       = "McCune, William",
    Year         = "2003",
    Title        = "{{\SC Otter} 3.3 Reference Manual}",
    note = "https://www.cs.unm.edu/~mccune/mace2/Otter33.pdf"
}

@article{blanchette-et-al-2016-isar,
  author    = {Jasmin Christian Blanchette and
               Sascha B{\"{o}}hme and
               Mathias Fleury and
               Steffen Juilf Smolka and
               Albert Steckermeier},
  title     = {Semi-intelligible Isar Proofs from Machine-Generated Proofs},
  journal   = {Journal of Automated Reasoning},
  volume    = {56},
  number    = {2},
  pages     = {155--200},
  year      = {2016},
  url       = {https://doi.org/10.1007/s10817-015-9335-3},
  XXXdoi       = {10.1007/s10817-015-9335-3},
}

@inproceedings{johansson-et-al-2014,
  author    = {Moa Johansson and
               Dan Ros{\'{e}}n and
               Nicholas Smallbone and
               Koen Claessen},
  title     = {Hipster: Integrating Theory Exploration in a Proof Assistant},
  booktitle = {Conference on Intelligent Computer Mathematics ({CICM} 2014\/)},
  pages     = {108--122},
  year      = {2014},
  editor    = {Stephen M. Watt and
               James H. Davenport and
               Alan P. Sexton and
               Petr Sojka and
               Josef Urban},
  series    = {Lecture Notes in Computer Science},
  volume    = {8543},
  publisher = {Springer}
}

@inproceedings{sonnex-et-al-2012,
  author    = {William Sonnex and
               Sophia Drossopoulou and
               Susan Eisenbach},
  title     = {Zeno: An Automated Prover for Properties of Recursive Data Structures},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems ({TACAS} 2012\/)},
  pages     = {407--421},
  year      = {2012},
  editor    = {Cormac Flanagan and
               Barbara K{\"{o}}nig},
  series    = {Lecture Notes in Computer Science},
  volume    = {7214},
  publisher = {Springer}
}

@incollection{weidenbach-2001,
  author    = {Christoph Weidenbach},
  title     = {Combining Superposition, Sorts and Splitting},
  booktitle = {Handbook of Automated Reasoning},
  volume = 2,
  pages     = {1965--2013},
  year      = {2001},
  editor    = {John Alan Robinson and
               Andrei Voronkov},
  publisher = {Elsevier and {MIT} Press},
}

@inproceedings{ganzinger-et-al-2004,
  author    = {Harald Ganzinger and
               George Hagen and
               Robert Nieuwenhuis and
               Albert Oliveras and
               Cesare Tinelli},
  editor    = {Rajeev Alur and
               Doron Peled},
  title     = {{\dpllt}: Fast Decision Procedures},
  booktitle = {Computer Aided Verification (CAV 2004\/)},
  series    = {Lecture Notes in Computer Science},
  volume    = {3114},
  pages     = {175--188},
  publisher = {Springer},
  year      = {2004}
}

@article{nieuwenhuis-et-al-2006,
  author    = {Robert Nieuwenhuis and
               Albert Oliveras and
               Cesare Tinelli},
  title     = {Solving {SAT} and {SAT} Modulo Theories: From an abstract
               {Davis--Putnam--Logemann--Loveland} procedure to \dpllt},
  journal   = {J. {ACM}},
  volume    = {53},
  number    = {6},
  pages     = {937--977},
  year      = {2006},
}

@techreport{barrett-et-al-2015,
  author = "Clark Barrett and Pascal Fontaine and Cesare Tinelli",
  title = "The {SMT-LIB} Standard: Version 2.5",
  institution  = "University of Iowa",
  year = 2015,
  note = "Available at \url{http://smt-lib.org/}"}

@inproceedings{sutcliffe-et-al-2009,
  author    = {Geoff Sutcliffe and
               Christoph Benzm{\"{u}}ller and
               Chad E. Brown and
               Frank Theiss},
  title     = {Progress in the Development of Automated Theorem Proving for Higher-Order
               Logic},
  booktitle = {Conference on Automated Deduction (CADE-22\/)},
  pages     = {116--130},
  year      = {2009},
  editor    = {Renate A. Schmidt},
  series    = {Lecture Notes in Computer Science},
  volume    = {5663},
  publisher = {Springer}
}

@inproceedings{claessen-et-al-2015,
  author    = {Koen Claessen and
               Moa Johansson and
               Dan Ros{\'{e}}n and
               Nicholas Smallbone},
  title     = {{TIP:} {T}ons of {I}nductive {P}roblems},
  booktitle = {Conference on Intelligent Computer Mathematics ({CICM} 2015\/)},
  pages     = {333--337},
  year      = {2015},
  editor    = {Manfred Kerber and
               Jacques Carette and
               Cezary Kaliszyk and
               Florian Rabe and
               Volker Sorge},
  series    = {Lecture Notes in Computer Science},
  volume    = {9150},
  publisher = {Springer}
}

@inproceedings{wisniewski-et-al-2015,
  author    = {Max Wisniewski and
               Alexander Steen and
               Christoph Benzm{\"{u}}ller},
  title     = {{LeoPARD}---{A} Generic Platform for the Implementation of Higher-Order
               Reasoners},
  booktitle = {Conference on Intelligent Computer Mathematics ({CICM} 2015\/)},
  pages     = {325--330},
  year      = {2015},
  editor    = {Manfred Kerber and
               Jacques Carette and
               Cezary Kaliszyk and
               Florian Rabe and
               Volker Sorge},
  series    = {Lecture Notes in Computer Science},
  volume    = {9150},
  publisher = {Springer}
}

@inproceedings{ludwig-waldmann-2007,
  author    = {Michel Ludwig and
               Uwe Waldmann},
  title     = {An Extension of the {K}nuth--{B}endix Ordering with {LPO}-Like Properties},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning ({LPAR} 2007\/)},
  pages     = {348--362},
  year      = {2007},
  editor    = {Nachum Dershowitz and
               Andrei Voronkov},
  series    = {Lecture Notes in Computer Science},
  volume    = {4790},
  publisher = {Springer},
}

@inproceedings{yamada-et-al-2013,
  author    = {Akihisa Yamada and
               Keiichirou Kusakari and
               Toshiki Sakabe},
  title     = {Unifying the {K}nuth--{B}endix, recursive path and polynomial orders},
  booktitle = {Principles and Practice of Declarative
               Programming ({PPDP} '13\/)},
  pages     = {181--192},
  year      = {2013},
  editor    = {Ricardo Pe{\~{n}}a and
               Tom Schrijvers},
  publisher = {{ACM}},
}

@inproceedings{brauner-et-al-2007,
  author    = {Paul Brauner and
               Cl{\'{e}}ment Houtmann and
               Claude Kirchner},
  title     = {Principles of Superdeduction},
  booktitle = {Logic in Computer Science (LICS 2007\/)},
  pages     = {41--50},
  year      = {2007},
  publisher = {{IEEE} Computer Society},
  year      = {2007},
}

@article{mayr-nipkow-1998,
  author    = {Richard Mayr and
               Tobias Nipkow},
  title     = {Higher-Order Rewrite Systems and Their Confluence},
  journal   = {Theor. Comput. Sci.},
  volume    = {192},
  number    = {1},
  pages     = {3--29},
  year      = {1998},
}

@book{miller-nadathur-2012,
  title = "Programming with Higher-Order Logic",
  author = "Dale Miller and Gopalan Nadathur",
  year = "2012",
  publisher = "Cambridge University Press"}

@inproceedings{komendantskaya-power-2011,
  author    = {Ekaterina Komendantskaya and
               John Power},
  title     = {Coalgebraic Derivations in Logic Programming},
  booktitle = {Computer Science Logic ({CSL} 2011\/)},
  pages     = {352--366},
  year      = {2011},
  editor    = {Marc Bezem},
  series    = {LIPIcs},
  volume    = {12},
  publisher = {Schloss Dagstuhl---Leibniz-Zentrum f{\"u}r Informatik},
}

@book{polya-1954,
  author = {P{\'o}lya, George},
  publisher = {Princeton University Press},
  title = {Mathematics of Plausible Reasoning{\upshape, volumes 1 and 2}},
  year = {1954}
}

@inproceedings{reynolds-et-al-2015-synthesis,
  author    = {Andrew Reynolds and
               Morgan Deters and
               Viktor Kuncak and
               Cesare Tinelli and
               Clark W. Barrett},
  title     = {Counterexample-Guided Quantifier Instantiation for Synthesis in {SMT}},
  booktitle = {Computer Aided Verification (CAV 2015\/)},
  pages     = {198--216},
  year      = {2015},
  editor    = {Daniel Kroening and
               Corina S. Pasareanu},
  series    = {Lecture Notes in Computer Science},
  volume    = {9207},
  publisher = {Springer},
}

@inproceedings{fetting-loechner-1996,
  author    = {Roland Fettig and
               Bernd L{\"{o}}chner},
  title     = {Unification of Higher-Order patterns in a Simply Typed Lambda-Calculus
               with Finite Products and Terminal Type},
  booktitle = {Rewriting Techniques and Applications (RTA-96\/)},
  pages     = {347--361},
  year      = {1996},
  editor    = {Harald Ganzinger},
  series    = {Lecture Notes in Computer Science},
  volume    = {1103},
  publisher = {Springer},
}

%%% TODO: Check
@article{benzmueller-et-al-201x,
  author = "Christoph Benzm{\"u}ller and Nik Sultana and Lawrence C. Paulson and Frank Thei{\ss}",
  title = "The Higher-Order Prover {{\SC {Leo-II}}}",
  journal   = {J.~Automated Reasoning},
  year = 2015}

@inproceedings{eggers-et-al-2011,
  author    = {Andreas Eggers and
               Evgeny Kruglov and
               Stefan Kupferschmid and
               Karsten Scheibler and
               Tino Teige and
               Christoph Weidenbach},
  title     = {Superposition Modulo Non-linear Arithmetic},
  booktitle = {Frontiers of Combining Systems (FroCoS~2011\/)},
  year      = {2011},
  pages     = {119--134},
  editor    = {Cesare Tinelli and
               Viorica Sofronie-Stokkermans},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6989}
}

@inproceedings{althaus-et-al-2009,
  author    = {Ernst Althaus and
               Evgeny Kruglov and
               Christoph Weidenbach},
  title     = {Superposition Modulo Linear Arithmetic {SUP(LA)}},
  booktitle = {Frontiers of Combining Systems (FroCoS~2009\/)},
  pages     = {84--99},
  editor    = {Silvio Ghilardi and
               Roberto Sebastiani},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5749},
  year      = {2009}
}

@inproceedings{azmy-weidenbach-2013,
  author    = {Noran Azmy and
               Christoph Weidenbach},
  title     = {Computing Tiny Clause Normal Forms},
  booktitle = {Conference on Automated Deduction (CADE-24\/)},
  year = 2013,
  pages     = {109--125},
  editor    = {Maria Paola Bonacina},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7898}
}

@inproceedings{blanchette-et-al-2014-compl,
  title = "Unified classical logic completeness: A coinductive pearl",
  author = "Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel",
  booktitle = {International Joint Conference on Automated Reasoning (IJCAR~2014\/)},
  pages     = {46--60},
  editor    = {St{\'e}phane Demri and
               Deepak Kapur and
               Christoph Weidenbach},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {8562},
  year      = {2014},
}

@inproceedings{barrett-et-al-2011-cvc4,
  author    = {Clark Barrett and
               Christopher L. Conway and
               Morgan Deters and
               Liana Hadarean and
               Dejan Jovanovi\'c and
               Tim King and
               Andrew Reynolds and
               Cesare Tinelli},
  title     = {{CVC4}},
  booktitle = {Computer Aided Verification (CAV~2011\/)},
  pages     = {171--177},
  year      = {2011},
  editor    = {Ganesh Gopalakrishnan and
               Shaz Qadeer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6806},
  publisher = {Springer},
}

@article{dowek-et-al-2003,
  author    = {Gilles Dowek and
               Th{\'{e}}r{\`{e}}se Hardin and
               Claude Kirchner},
  title     = {Theorem Proving Modulo},
  journal   = {J.~Automated Reasoning},
  volume    = {31},
  number    = {1},
  pages     = {33--72},
  year      = {2003}
}

@inproceedings{sturm-weispfenning-1996,
  author    = {Thomas Sturm and
               Volker Weispfenning},
  title     = {Computational Geometry Problems in {REDLOG}},
  booktitle = {Automated Deduction in Geometry (ADG '96)},
  pages     = {58--86},
  editor    = {Dongming Wang},
  series    = {Lecture Notes in Computer Science},
  volume    = {1360},
  publisher = {Springer},
  year      = {1997}
}

@inproceedings{jaroschek-et-al-2015,
  author    = {Maximilian Jaroschek and
               Pablo Federico Dobal and
               Pascal Fontaine},
  title     = {Adapting Real Quantifier Elimination Methods for Conflict Set Computation},
  booktitle = {Frontiers of Combining Systems (FroCoS~2015\/)},
  pages     = {151--166},
  year      = {2015},
  editor    = {Carsten Lutz and
               Silvio Ranise},
  series    = {Lecture Notes in Computer Science},
  volume    = {9322},
  publisher = {Springer}
}

@inproceedings{baumgartner-et-al-2014,
  author    = {Peter Baumgartner and
               Joshua Bax and
               Uwe Waldmann},
  title     = {Finite Quantification in Hierarchic Theorem Proving},
  booktitle = {International Joint Conference on Automated Reasoning ({IJCAR} 2014\/)},
  pages     = {152--167},
  year      = {2014},
  editor    = {St{\'{e}}phane Demri and
               Deepak Kapur and
               Christoph Weidenbach},
  series    = {Lecture Notes in Computer Science},
  volume    = {8562},
  publisher = {Springer},
}

@inproceedings{bourke-et-al-2012,
  author    = {Timothy Bourke and
               Matthias Daum and
               Gerwin Klein and
               Rafal Kolanski},
  title     = {Challenges and Experiences in Managing Large-Scale Proofs},
  booktitle     = {Conference on Intelligent Computer Mathematics (CICM 2012\/)},
  pages     = {32--48},
  year      = {2012},
  editor    = {Johan Jeuring and
               John A. Campbell and
               Jacques Carette and
               Dos Reis, Gabriel and
               Petr Sojka and
               Makarius Wenzel and
               Volker Sorge},
  series    = {Lecture Notes in Computer Science},
  volume    = {7362},
  publisher = {Springer},
}

@inproceedings{krings-et-al-2015,
  author    = {Sebastian Krings and
               Jens Bendisposto and
               Michael Leuschel},
  title     = {From Failure to Proof: The {ProB} Disprover for {B} and Event-B},
  booktitle = {Software Engineering and Formal Methods ({SEFM} 2015\/)},
  pages     = {199--214},
  year      = {2015},
  editor    = {Radu Calinescu and
               Bernhard Rumpe},
  series    = {Lecture Notes in Computer Science},
  volume    = {9276},
  publisher = {Springer},
}

@inproceedings{baumgartner-bax-2013,
  author    = {Peter Baumgartner and
               Joshua Bax},
  title     = {Proving Infinite Satisfiability},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 19th
               International Conference, LPAR-19, Stellenbosch, South Africa, December
               14-19, 2013. Proceedings},
  pages     = {86--95},
  editor    = {Kenneth L. McMillan and
               Aart Middeldorp and
               Andrei Voronkov},
  series    = {Lecture Notes in Computer Science},
  volume    = {8312},
  publisher = {Springer},
  year      = {2013}
}

@inproceedings{armand-et-al-2011,
  author    = {Micha{\"{e}}l Armand and
               Germain Faure and
               Benjamin Gr{\'{e}}goire and
               Chantal Keller and
               Laurent Th{\'{e}}ry and
               Benjamin Werner},
  title     = {A Modular Integration of {SAT/SMT} Solvers to {C}oq through Proof Witnesses},
  booktitle = {Certified Programs and Proofs (CPP 2011\/)},
  pages     = {135--150},
  year      = {2011},
  editor    = {Jean-Pierre Jouannaud and
               Zhong Shao},
  series    = {Lecture Notes in Computer Science},
  volume    = {7086},
  publisher = {Springer},
}

@inproceedings{otten-2008,
  author    = {Jens Otten},
  title     = {{leanCoP} 2.0 and {ileanCoP} 1.2: High Performance Lean Theorem Proving
               in Classical and Intuitionistic Logic (System Descriptions)},
  booktitle = {International Joint Conference on Automated Reasoning ({IJCAR} 2008\/)},
  pages     = {283--291},
  year      = {2008},
  editor    = {Alessandro Armando and
               Peter Baumgartner and
               Gilles Dowek},
  series    = {Lecture Notes in Computer Science},
  volume    = {5195},
  publisher = {Springer}
}

@inproceedings{gonthier-et-al-2013,
  author    = {Georges Gonthier and
               Andrea Asperti and
               Jeremy Avigad and
               Yves Bertot and
               Cyril Cohen and
               Fran{\c{c}}ois Garillot and
               St{\'{e}}phane Le Roux and
               Assia Mahboubi and
               Russell O'Connor and
               Sidi Ould Biha and
               Ioana Pasca and
               Laurence Rideau and
               Alexey Solovyev and
               Enrico Tassi and
               Laurent Th{\'{e}}ry},
  title     = {A~Machine-Checked Proof of the Odd Order Theorem},
  booktitle = {Interactive Theorem Proving (ITP 2013\/)},
  pages     = {163--179},
  year      = {2013},
  editor    = {Sandrine Blazy and
               Christine Paulin{-}Mohring and
               David Pichardie},
  series    = {Lecture Notes in Computer Science},
  volume    = {7998},
  publisher = {Springer},
  note = "DOI: 10.1007/978-3-642-39634-2\_14"}
}

@inproceedings{merz-vanzetto-2014,
  author    = {Stephan Merz and
               Hern{\'{a}}n Vanzetto},
  title     = {Refinement Types for {\tlaplus}},
  booktitle = {{NASA} Formal Methods ({NFM} 2014)},
  pages     = {143--157},
  year      = {2014},
  editor    = {Julia M. Badger and
               Kristin Yvonne Rozier},
  series    = {Lecture Notes in Computer Science},
  volume    = {8430},
  publisher = {Springer},
}

@inproceedings{chlipala-necula-2006,
  author = "Adam Chlipala and George C. Necula",
  title = "Cooperative Integration of an Interactive Proof Assistant and an Automated Prover",
  booktitle = "Workshop on Strategies in Automated Deduction (STRATEGIES '06\/)",
  year = 2006}

@article{ganzinger-stuber-2005,
  author    = {Harald Ganzinger and
               J{\"{u}}rgen Stuber},
  title     = {Superposition with equivalence reasoning and delayed clause normal
               form transformation},
  journal   = {Information and Computation},
  volume    = {199},
  number    = {1--2},
  pages     = {3--23},
  year      = {2005},
}

@incollection{benzmueller-miller-2014,
  author    = {Christoph Benzm{\"{u}}ller and
               Dale Miller},
  title     = {Automation of Higher-Order Logic},
  booktitle = {Computational Logic},
  pages     = {215--254},
  year      = {2014},
  editor    = {J{\"{o}}rg H. Siekmann},
  title     = {Computational Logic},
  series    = {Handbook of the History of Logic},
  volume    = {9},
  publisher = {Elsevier},
  year      = {2014},
  isbn      = {978-0-444-51624-4},
  timestamp = {Mon, 29 Jun 2015 15:11:00 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/series/hhl/9},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@misc{blanchette-et-al-isafol,
  author =
    "Jasmin Christian Blanchette and
     Mathias Fleury and
     Anders Schlichtkrull and
     Dmitriy Traytel",
  title = "\isafol: {I}sabelle {F}ormalization of {L}ogic",
  note = "\url{https://bitbucket.org/jasmin_blanchette/isafol}"}

@misc{sternagel-thiemann-isafor,
  author = "Christian Sternagel and Ren\'e Thiemann",
  title = "An {Isabelle/HOL} Formalization of Rewriting for Certified Termination Analysis",
  note = "\url{http://cl-informatik.uibk.ac.at/software/ceta/}"}

@inproceedings{krauss-et-al-2011,
  author    = {Alexander Krauss and
               Christian Sternagel and
               Ren{\'{e}} Thiemann and
               Carsten Fuhs and
               J{\"{u}}rgen Giesl},
  title     = {Termination of {I}sabelle Functions via Termination of Rewriting},
  booktitle = {Interactive Theorem Proving ({ITP} 2011)},
  pages     = {152--167},
  year      = {2011},
  editor    = {Marko C. J. D. van~Eekelen and
               Herman Geuvers and
               Julien Schmaltz and
               Freek Wiedijk},
  series    = {Lecture Notes in Computer Science},
  volume    = {6898},
  publisher = {Springer},
  year      = {2011}
}

@inproceedings{de-moura-bjoerner-2008-plus-saturation,
  author    = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  title     = {Engineering {\dpllt} + Saturation},
  booktitle = {International Joint Conference on Automated Reasoning ({IJCAR} 2008)},
  pages     = {475--490},
  year      = {2008},
  editor    = {Alessandro Armando and
               Peter Baumgartner and
               Gilles Dowek},
  series    = {Lecture Notes in Computer Science},
  volume    = {5195},
  publisher = {Springer},
}

@inproceedings{baumgartner-tinelli-2011,
  author    = {Peter Baumgartner and
               Cesare Tinelli},
  title     = {Model Evolution with Equality Modulo Built-in Theories},
  booktitle = {Conference on Automated Deduction ({CADE-23})},
  pages     = {85--100},
  year      = {2011},
  editor    = {Nikolaj Bj{\o}rner and
               Viorica Sofronie{-}Stokkermans},
  series    = {Lecture Notes in Computer Science},
  volume    = {6803},
  publisher = {Springer},
}

@article{jouannaud-rubio-2007,
  author    = {Jean{-}Pierre Jouannaud and
               Albert Rubio},
  title     = {Polymorphic higher-order recursive path orderings},
  journal   = {J. {ACM}},
  volume    = {54},
  number    = {1},
  year      = {2007},
}

@inproceedings{barbosa-fontaine-2015,
  author = "Haniel Barbosa and Pascal Fontaine",
  title = "Congruence Closure with Free Variables (Work in Progress)",
  booktitle = {Workshop on Quantification (QUANTIFY 2015\/)},
  editor = "Hubie Chen and Florian Lonsing and Martina Seidl",
  year = 2015,
  note = "Available at \url{http://www.loria.fr/~hbarbosa/quantify2015.pdf}"}

@inproceedings{blanchette-et-al-2015-wit,
  author    = {Jasmin Christian Blanchette and
               Andrei Popescu and
               Dmitriy Traytel},
  title     = {Witnessing (Co)datatypes},
  booktitle = {European Symposium on Programming Languages and Systems
    ({ESOP} 2015\/)},
  pages     = {359--382},
  year      = {2015},
  editor    = {Jan Vitek},
  series    = {Lecture Notes in Computer Science},
  volume    = {9032},
  publisher = {Springer}
}

@inproceedings{blanchette-et-al-2015-afp,
  title = "Mining the {A}rchive of {F}ormal {P}roofs",
  author = {Jasmin Christian Blanchette and Maximilian Haslbeck and Daniel Matichuk and Tobias Nipkow},
  booktitle = "Conference on Intelligent Computer Mathematics (CICM 2015\/)",
  editor = "Manfred Kerber",
  series = "Lecture Notes in Computer Science",
  volume = 9150,
  pages = "1--15",
  publisher = "Springer",
  year = 2015}

@book{nederpelt-et-al-1994,
    editor = {Nederpelt, Rob and Geuvers, Herman and de Vrijer, Roel},
    publisher = {Elsevier Science},
    series = {Studies in Logic and the Foundations of Mathematics},
    title = {Selected Papers on Automath},
    volume = {133},
    year = {1994}
}

@article{harrison-thery-1998,
  author    = {John Harrison and
               Laurent Th{\'{e}}ry},
  title     = {A Skeptic's Approach to Combining {HOL} and {M}aple},
  journal   = {J.~Automated Reasoning},
  volume    = {21},
  number    = {3},
  pages     = {279--294},
  year      = {1998}
}

@article{bertoli-et-al-1999,
  author    = {Piergiorgio Bertoli and
               Jacques Calmet and
               Fausto Giunchiglia and
               Karsten Homann},
  title     = {Specification and Integration of Theorem Provers and Computer Algebra
               Systems},
  journal   = {Fundamenta Informaticae},
  volume    = {39},
  number    = {1--2},
  pages     = {39--57},
  year      = {1999}
}

@inproceedings{lewis-2017-leanmm,
  title = "An extensible ad hoc interface between {L}ean and {M}athematica",
  author = "Robert Y. Lewis",
  XXXyear = 2017,
  editor = "Catherine Dubois and Woltzenlogel Paleo, Bruno",
  series    = {EPTCS},
  booktitle = "Proof Exchange for Theorem Proving (PxTP 2017)",
  note = "To appear"}

http://www.nature.com/news/the-biggest-mystery-in-mathematics-shinichi-mochizuki-and-the-impenetrable-proof-1.18509

@article{castelvecchi-2015,
  title = "The biggest mystery in mathematics: {S}hinichi {M}ochizuki and the impenetrable proof",
  author = "Davide Castelvecchi",
  journal = "Nature",
  year = 2015,
  volume = 526,
  page = "178--181",
  note = "DOI: 10.1038/526178a"
}

@inproceedings{nipkow-2012-lsd,
  author    = {Tobias Nipkow},
  title     = {Teaching Semantics with a Proof Assistant: No More {LSD} Trip Proofs},
  booktitle = {Verification, Model Checking, and Abstract Interpretation ({VMCAI}~2012)},
  pages     = {24--38},
  editor    = {Viktor Kuncak and
               Andrey Rybalchenko},
  series    = {Lecture Notes in Computer Science},
  volume    = {7148},
  publisher = {Springer},
  year      = {2012}
}

@misc{wiedijk-2016-dagstuhl,
  title = "Computation in Proofs",
  author = "Freek Wiedijk",
  howpublished = "Presented at \emph{Dagstuhl Seminar on the Universality of Proofs}",
  xxxeditors = "XXX",
  year = 2016}

@misc{sewell-2017-big-proof,
  title = "Contribution to the panel on future directions for Big Proof",
  author = "Peter Sewell",
  howpublished = "Presented at \emph{Workshop on Computer-Aided Mathematical Proof}",
  xxxeditors = "Ursula Martin and Larry Paulson and Andrew Pitts",
  year = 2017,
  note = "Video available at \url{https://www.newton.ac.uk/seminar/20170714143015301}"
}

@misc{davenport-2017-big-proof,
  title = "Computer Algebra and Formal Proof",
  author = "James Davenport",
  howpublished = "Presented at \emph{Big Proof Programme}",
  xxxeditors = "Jeremy Avigad and Natarajan Shankar and Leonardo de Moura and
    Georges Gonthier and Ursula Martin and J Strother Moore and
    Lawrence Paulson and Andrew Pitts",
  year = 2017,
  note = "Video available at \url{https://www.newton.ac.uk/seminar/20170721110012002}"
}

@misc{hales-2017-big-proof,
  title = "Big Conjectures",
  author = "Thomas Hales",
  howpublished = "Presented at \emph{Workshop on Computer-Aided Mathematical Proof}",
  xxxeditors = "Ursula Martin and Larry Paulson and Andrew Pitts",
  year = 2017,
  note = "Video available at \url{https://www.newton.ac.uk/seminar/20170710100011001}"
}

@misc{gonthier-2017-big-proof,
  title = "Scaffolds and frames: The {MathComp} algebra formal library",
  author = "Georges Gonthier",
  howpublished = "Presented at \emph{Workshop on Computer-Aided Mathematical Proof}",
  xxxeditors = "Ursula Martin and Larry Paulson and Andrew Pitts",
  year = 2017,
  note = "Video available at \url{https://www.newton.ac.uk/seminar/20170713090010001}"
}

@article{boldo-et-al-2013,
  author    = {Sylvie Boldo and
               Fran{\c{c}}ois Cl{\'{e}}ment and
               Jean{-}Christophe Filli{\^{a}}tre and
               Micaela Mayero and
               Guillaume Melquiond and
               Pierre Weis},
  title     = {Wave Equation Numerical Resolution: {A} Comprehensive Mechanized Proof
               of a {C} Program},
  journal   = {J.~Automated Reasoning},
  volume    = {50},
  number    = {4},
  pages     = {423--456},
  year      = {2013},
  url       = {https://doi.org/10.1007/s10817-012-9255-4},
  XXXdoi       = {10.1007/s10817-012-9255-4},
  timestamp = {Sat, 20 May 2017 00:22:32 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jar/BoldoCFMMW13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{hoelzl-2016,
  author    = {Johannes H{\"{o}}lzl},
  editor    = {Jasmin Christian Blanchette and
               Stephan Merz},
  title     = {Formalising Semantics for Expected Running Time of Probabilistic Programs},
  booktitle = "Interactive Theorem Proving (ITP 2016\/)",
  series    = {Lecture Notes in Computer Science},
  volume    = {9807},
  pages     = {475--482},
  publisher = {Springer},
  year      = {2016}
}

@techreport{thery-2007,
  author = "Laurent Th\'ery",
  title = "Proving the group law for elliptic curves formally",
  XXXnumber = "RT-0330",
  institution = "INRIA",
  year = 2007,
  publisher = "\url{https://hal.inria.fr/inria-00129237}"
}

@inproceedings{de-moura-et-al-2015,
  author    = {Leonardo de Moura and
               Soonho Kong and
               Jeremy Avigad and
               Floris van Doorn and
               Jakob von Raumer},
  editor    = {Amy P. Felty and
               Aart Middeldorp},
  title     = {The {L}ean Theorem Prover (System Description)},
  booktitle = {Conference on Automated Deduction ({CADE-25})},
  series    = {Lecture Notes in Computer Science},
  volume    = {9195},
  pages     = {378--388},
  publisher = {Springer},
  year      = {2015},
  note = "DOI: 10.1007/978-3-319-21401-6\_26"
}

@article{barthe-et-al-2003,
  author    = {Gilles Barthe and
               Venanzio Capretta and
               Olivier Pons},
  title     = {Setoids in type theory},
  journal   = {Journal of Functional Programming},
  volume    = {13},
  number    = {2},
  year      = {2003},
  pages     = {261--293},
  note = "DOI: 10.1017/S0956796802004501"
}

@article{pelayo-et-al-2013,
  author    = {{\'{A}}lvaro Pelayo and
               Vladimir Voevodsky and
               Michael A. Warren},
  title     = {A preliminary univalent formalization of the \textit{p}-adic numbers},
  journal   = {CoRR},
  volume    = {abs/1302.1207},
  year      = {2013}
}

@article{pelayo-et-al-2015,
  author    = {{\'{A}}lvaro Pelayo and
               Vladimir Voevodsky and
               Michael A. Warren},
  title     = {A univalent formalization of the \textit{p}-adic numbers},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {25},
  number    = {5},
  pages     = {1147--1171},
  year      = {2015}
}

@incollection{awodey-2012,
  author    = {Steven Awodey},
  editor    = {Peter Dybjer and
               Sten Lindstr{\"{o}}m and
               Erik Palmgren and
               G{\"{o}}ran Sundholm},
  title     = {Type Theory and Homotopy},
  booktitle = {Epistemology versus Ontology---Essays on the Philosophy and Foundations
               of Mathematics in Honour of Per Martin-L{\"{o}}f},
  series    = {Logic, Epistemology, and the Unity of Science},
  volume    = {27},
  pages     = {183--201},
  publisher = {Springer},
  year      = {2012},
  note = "DOI: 10.1007/978-94-007-4435-6\_9"
}

@article{avigad-et-al-201x-clt,
  title = "A Formally Verified Proof of the {C}entral {L}imit {T}heorem",
  author = {Jeremy Avigad and Johannes H\"olzl and Luke Serafin},
  journal = {J.~Automated Reasoning},
  note = "To appear"}


%%% TODO: Complete
@inproceedings{bentkamp-et-al-2017-itp,
  title = "A formal proof of the expressiveness of deep learning",
  author = "Alexander Bentkamp and J. C. Blanchette and Dietrich Klakow",
  editor = "Mauricio Ayala-Rinc\'on and C\'esar A. Mu{\~n}os",
  booktitle = "Interactive Theorem Proving (ITP 2017\/)",
  pages = "46--64",
  volume = 10499,
  series = "Lecture Notes in Computer Science",
  publisher = "Springer",
  year = 2017}

@article{stothers-1981,
  author = "W. W. Stothers",
  title = "Polynomial identities and hauptmoduln",
  journal = "Quarterly J. Mathematics Oxford",
  volume = 32,
  number = 2,
  page = "349--370"}

@book{mason-1984,
  author = "Mason, R. C.",
  year = 1984,
  title = "Diophantine Equations over Function Fields",
  series = "London Mathematical Society Lecture Note Series",
  number = 96,
  publisher = "Cambridge University Press"}

@article{cohn-elkies-2003,
  title = "New upper bounds on sphere packings {I}",
  author = "Henry Cohn and Noam Elkies",
  journal = "Ann. Math. II",
  volume = 157,
  year = 2003,
  pages = "689--714"}

@article{heule-kullmann-2017,
  author    = {Marijn J. H. Heule and
               Oliver Kullmann},
  title     = {The science of brute force},
  journal   = {Communications of the {ACM}},
  volume    = {60},
  number    = {8},
  pages     = {70--79},
  year      = {2017}
}

@book{stewart-tall-2015,
  title={Algebraic Number Theory and Fermat's Last Theorem},
  edition = "fourth",
  author={Stewart, Ian and Tall, David},
  url={https://books.google.no/books?id=PIibasv45boC},
  year={2001},
  publisher={CRC Press, Taylor \& Francis Group}
}

@book{cohen-2000-course,
    AUTHOR = {Cohen, Henri},
     TITLE = {A course in computational algebraic number theory},
    SERIES = {Graduate Texts in Mathematics},
    VOLUME = {138},
 PUBLISHER = {Springer-Verlag, Berlin},
      YEAR = {1993},
     PAGES = {xii+534},
      ISBN = {3-540-55640-0},
   MRCLASS = {11Y40 (11Rxx 68Q40)},
  MRNUMBER = {1228206},
MRREVIEWER = {Joe\ P.\ Buhler},
       DOI = {10.1007/978-3-662-02945-9},
       URL = {https://doi.org/10.1007/978-3-662-02945-9},
       note = {DOI: 10.1007/978-3-662-02945-9},
}


@book{cohen-2007-advanced,
  author = "Henri Cohen",
  title = "Advanced Topics in Computational Number Theory",
  year = "2007",
  volume = "240",
  series = "Graduate Texts in Mathematics",
  publisher = "Springer"}

@inproceedings{adams-et-al-2001,
  author    = {Andrew Adams and
               Martin Dunstan and
               Hanne Gottliebsen and
               Tom Kelsey and
               Ursula Martin and
               Sam Owre},
  editor    = {Richard J. Boulton and
               Paul B. Jackson},
  title     = {Computer Algebra Meets Automated Theorem Proving: Integrating {M}aple
               and {PVS}},
  booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2001)},
  series    = {Lecture Notes in Computer Science},
  volume    = {2152},
  pages     = {27--42},
  publisher = {Springer},
  year      = {2001}
}

@inproceedings{cohen-2012,
  author    = {Cyril Cohen},
  editor    = {Lennart Beringer and
               Amy P. Felty},
  title     = {Construction of Real Algebraic Numbers in Coq},
  booktitle = {Interactive Theorem Proving ({ITP} 2012)},
  series    = {Lecture Notes in Computer Science},
  volume    = {7406},
  pages     = {67--82},
  publisher = {Springer},
  year      = {2012}
}

@inproceedings{thiemann-yamada-2016,
  author    = {Ren{\'{e}} Thiemann and
               Akihisa Yamada},
  editor    = {Jasmin Christian Blanchette and
               Stephan Merz},
  title     = {Algebraic Numbers in {I}sabelle/{HOL}},
  booktitle = {Interactive Theorem Proving ({ITP} 2016)},
  series    = {Lecture Notes in Computer Science},
  volume    = {9807},
  pages     = {391--408},
  publisher = {Springer},
  year      = {2016}
}

@phdthesis{moertberg-2012,
  author = {Anders M\"ortberg},
  title = "Constructive Algebra in Type Theory",
  year = 2012,
  school = {Chalmers tekniska h\"ogskola},
  type = "Licentiate thesis",
  note = "Available at \url{http://www-sop.inria.fr/members/Anders.Mortberg/papers/licentiate_thesis.pdf}"}

@inproceedings{oconnor-2008,
  author    = {Russell O'Connor},
  editor    = {Otmane A{\"{\i}}t Mohamed and
               C{\'{e}}sar A. Mu{\~{n}}oz and
               Sofi{\`{e}}ne Tahar},
  title     = {Certified Exact Transcendental Real Number Computation in {C}oq},
  booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2008)},
  series    = {Lecture Notes in Computer Science},
  volume    = {5170},
  pages     = {246--261},
  publisher = {Springer},
  year      = {2008}
}

@inproceedings{garillot-et-al-2009,
  author    = {Fran{\c{c}}ois Garillot and
               Georges Gonthier and
               Assia Mahboubi and
               Laurence Rideau},
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  title     = {Packaging Mathematical Structures},
  booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2009)},
  series    = {Lecture Notes in Computer Science},
  volume    = {5674},
  pages     = {327--342},
  publisher = {Springer},
  year      = {2009}
}

@inproceedings{menes-et-al-2012,
  author    = {Maxime D{\'{e}}n{\`{e}}s and
               Anders M{\"{o}}rtberg and
               Vincent Siles},
  editor    = {Lennart Beringer and
               Amy P. Felty},
  title     = {A Refinement-Based Approach to Computational Algebra in {C}oq},
  booktitle = {Interactive Theorem Proving ({ITP}~2012)},
  series    = {Lecture Notes in Computer Science},
  volume    = {7406},
  pages     = {83--98},
  publisher = {Springer},
  year      = {2012}
}

@inproceedings{eberl-2015,
  author    = {Manuel Eberl},
  editor    = {Xavier Leroy and
               Alwen Tiu},
  title     = {A Decision Procedure for Univariate Real Polynomials in {I}sabelle/{HOL}},
  booktitle = {Certified Programs and Proofs ({CPP} 2015)},
  pages     = {75--83},
  publisher = {{ACM}},
  year      = {2015}
}

@inproceedings{paulson-2017-cpp,
  author    = {Lawrence C. Paulson},
  editor    = {Yves Bertot and
               Viktor Vafeiadis},
  title     = {Porting the {HOL} {L}ight analysis library: Some lessons (invited talk)},
  booktitle = {Certified Programs and Proofs ({CPP} 2017)},
  pages     = {1},
  publisher = {{ACM}},
  year      = {2017},
  note = "DOI: 10.1145/3018610.3023366"
}

@article{sturm-weispfenning-2004,
  title = "P-adic Root Isolation",
  author = "Thomas Sturm and Volker Weispfenning",
  journal = "Revista de la Real Academia de Ciencias Exactas, F{\'\i}sicas y Naturales, Serie A",
  volume = 98,
  number = 1,
  year = 2004,
  pages = "239--258"}

@inproceedings{ebner-et-al-2017,
  author    = {Gabriel Ebner and Sebastian Ullrich and Jared Roesch and Jeremy Avigad and Leonardo de Moura},
  title     = {A Metaprogramming Framework for Formal Verification},
  booktitle = {International Conference on Functional Programming ({ICFP} 2017\/)},
  pages     = {34:1--34:29},
  year      = {2017},
  XXXeditor    = {Mark Jones},
  publisher = {{ACM}},
  note = "DOI: 10.1145/3110278"
}

@inproceedings{weispfenning-1983,
  author = "Volker Weispfenning",
  title = "Quantifier elimination and decision procedures for valued fields",
  editor = {Richter, M.M. and B\"orger, E. and Oberschelp, W. and Schinzel, B. and Thomas, W.},
  booktitle = "Logic Colloquium 1983",
  series = "Lecture Notes in Mathematics",
  volume = 1103,
  publisher = "Springer",
  year = 1984,
  pages = "419--472"}

@inproceedings{cruanes-blanchette-2016,
  author    = {Simon Cruanes and
               Jasmin Christian Blanchette},
  editor    = {Jasmin Christian Blanchette and
               Cezary Kaliszyk},
  title     = {Extending {N}unchaku to Dependent Type Theory},
  booktitle = {Workshop on Hammers for Type Theories (HaTT~2016)},
  series    = {{EPTCS}},
  volume    = {210},
  pages     = {3--12},
  year      = {2016},
  note = {DOI: 10.4204/EPTCS.210.3}
}

@inproceedings{reynolds-et-al-2016,
  author    = {Andrew Reynolds and
               Jasmin Christian Blanchette and
               Simon Cruanes and
               Cesare Tinelli},
  editor    = {Nicola Olivetti and
               Ashish Tiwari},
  title     = {Model Finding for Recursive Functions in {SMT}},
  booktitle = {International Joint Conference on Automated Reasoning ({IJCAR}
               2016)},
  series    = {Lecture Notes in Computer Science},
  volume    = {9706},
  pages     = {133--151},
  publisher = {Springer},
  year      = {2016}
}

@article{avigad-et-al-2016,
  author    = {Jeremy Avigad and
               Robert Y. Lewis and
               Cody Roux},
  title     = {A Heuristic Prover for Real Inequalities},
  journal   = {J.~Automated Reasoning},
  volume    = {56},
  number    = {3},
  pages     = {367--386},
  year      = {2016}
}

@inproceedings{selsam-de-moura-2016,
  author    = {Daniel Selsam and
               Leonardo de Moura},
  editor    = {Nicola Olivetti and
               Ashish Tiwari},
  title     = {Congruence Closure in Intensional Type Theory},
  booktitle = {International Joint Conference on Automated Reasoning ({IJCAR}
               2016)},
  series    = {Lecture Notes in Computer Science},
  volume    = {9706},
  pages     = {99--115},
  publisher = {Springer},
  year      = {2016}
}

@inproceedings{de-moura-bjoerner-2007,
  author    = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  editor    = {Frank Pfenning},
  title     = {Efficient E-Matching for {SMT} Solvers},
  booktitle = {Conference on Automated Deduction (CADE-21)},
  series    = {Lecture Notes in Computer Science},
  volume    = {4603},
  pages     = {183--198},
  publisher = {Springer},
  year      = {2007}
}

@InProceedings{schulz-2014,
 author =       {Stephan Schulz},
 title =        {System Description: {E}~1.8},
 booktitle =    {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19)},
 pages =     {735--743},
 year =         {2013},
 editor =       {Ken McMillan and Aart Middeldorp and Andrei Voronkov},
 volume =       {8312},
 series={{Lecture Notes in Computer Science}},
 publisher =    {Springer}
}

@inproceedings{benzmueller-et-al-2017,
  author    = {Christoph Benzm{\"{u}}ller and
               Alexander Steen and
               Max Wisniewski},
  editor    = {Thomas Eiter and
               David Sands and
               Geoff Sutcliffe and
               Andrei Voronkov},
  title     = {{Leo-III} Version 1.1 (System description)},
  booktitle = {International Workshop on the Implementation of Logics (IWIL-2017)},
  series    = {Kalpa Publications in Computing},
  volume    = {1},
  publisher = {EasyChair},
  year      = {2017}
}

@inproceedings{blanchette-et-al-2014-truly,
  author    = {Jasmin Christian Blanchette and
               Johannes H{\"{o}}lzl and
               Andreas Lochbihler and
               Lorenz Panny and
               Andrei Popescu and
               Dmitriy Traytel},
  editor    = {Gerwin Klein and
               Ruben Gamboa},
  title     = {Truly Modular (Co)datatypes for {I}sabelle/{HOL}},
  booktitle = {Interactive Theorem Proving ({ITP} 2014)},
  series    = {Lecture Notes in Computer Science},
  volume    = {8558},
  pages     = {93--110},
  publisher = {Springer},
  year      = {2014}
}

@book{russell-1919,
  author = "Bertrand Russell",
  title = "Introduction to Mathematical Philosophy",
  series = "The Library of Philosophy",
  publisher = "Allen and Unwin and the Macmillan Company",
  year = 1919}

@article {breuil-et-al-2001,
    AUTHOR = {Breuil, Christophe and Conrad, Brian and Diamond, Fred and
              Taylor, Richard},
     TITLE = {On the modularity of elliptic curves over \textbf{Q}: Wild
              3-adic exercises},
   JOURNAL = {J. American Mathematical Society},
    VOLUME = {14},
      YEAR = {2001},
    NUMBER = {4},
     PAGES = {843--939}
}

@article {wiles-1995,
    AUTHOR = {Wiles, Andrew},
     TITLE = {Modular elliptic curves and {F}ermat's last theorem},
  journal = "Ann. Math. II",
    VOLUME = {141},
      YEAR = {1995},
    NUMBER = {3},
     PAGES = {443--551}
}

@inproceedings{kohlhase-2012,
  author    = {Michael Kohlhase},
  editor    = {Andrei Voronkov and
               Viorel Negru and
               Tetsuo Ida and
               Tudor Jebelean and
               Dana Petcu and
               Stephen M. Watt and
               Daniela Zaharie},
  title     = {The Flexiformalist Manifesto},
  booktitle = {Symbolic and Numeric Algorithms for
               Scientific Computing ({SYNASC} 2012)},
  pages     = {30--35},
  publisher = {{IEEE} Computer Society},
  year      = {2012}
}

@article{bentkamp-2015-afp-latin,
  author    = {Alexander Bentkamp},
  title     = {Latin Square},
  journal   = {Archive of Formal Proofs},
  volume    = {2015},
  note       = {Available at \url{https://www.isa-afp.org/entries/Latin_Square.shtml}}
}

@inproceedings{hoelzl-heller-2011,
  author    = {Johannes H{\"{o}}lzl and
               Armin Heller},
  editor    = {Marko C. J. D. van~Eekelen and
               Herman Geuvers and
               Julien Schmaltz and
               Freek Wiedijk},
  title     = {Three Chapters of Measure Theory in {I}sabelle\slash {HOL}},
  booktitle = {Interactive Theorem Proving ({ITP} 2011)},
  series    = {Lecture Notes in Computer Science},
  volume    = {6898},
  pages     = {135--151},
  publisher = {Springer},
  year      = {2011}
}

@inproceedings{immler-hoelzl-2012,
  author    = {Fabian Immler and
               Johannes H{\"{o}}lzl},
  editor    = {Lennart Beringer and
               Amy P. Felty},
  title     = {Numerical Analysis of Ordinary Differential Equations in {I}sabelle/{HOL}},
  booktitle = {Interactive Theorem Proving ({ITP}~2012)},
  series    = {Lecture Notes in Computer Science},
  volume    = {7406},
  pages     = {377--392},
  publisher = {Springer},
  year      = {2012}
}

@misc{mahboubi-2017-big-proof,
  title = "Formally Verified Approximations of Definite Integrals",
  author = "Assia Mahboubi",
  howpublished = "Presented at \emph{Workshop on Computer-Aided Mathematical Proof}",
  xxxeditors = "Ursula Martin and Larry Paulson and Andrew Pitts",
  year = 2017,
  note = "Slides available at \url{https://www.newton.ac.uk/seminar/20170712090010001}"
}

@book{noag-ict-2005,
  editor = "M. Kas and F. Karelse",
  title = "Met vaste hand---Nationale Onderzoeksagenda Informatie en Communicatietechnologie (NOAG-ict) 2005--2010",
  publisher = "Albani drukkers",
  year = 2005
}

@inproceedings{xi-et-al-2014,
  author    = {Li Xi and
               Kang Yang and
               Zhenfeng Zhang and
               Dengguo Feng},
  editor    = {Thorsten Holz and
               Sotiris Ioannidis},
  title     = {{DAA}-Related {APIs} in {TPM} 2.0 Revisited},
  booktitle = {Trust and Trustworthy Computing ({TRUST}
               2014)},
  series    = {Lecture Notes in Computer Science},
  volume    = {8564},
  pages     = {1--18},
  publisher = {Springer},
  year      = {2014},
  note = "DOI: 10.1007/978-3-319-08593-7\_1"
}

@inproceedings{pass-et-al-2017,
  author    = {Rafael Pass and
               Elaine Shi and
               Florian Tram{\`{e}}r},
  editor    = {Jean{-}S{\'{e}}bastien Coron and
               Jesper Buus Nielsen},
  title     = {Formal Abstractions for Attested Execution Secure Processors},
  booktitle = {Advances in Cryptology ({EUROCRYPT}~2017)},
  series    = {Lecture Notes in Computer Science},
  volume    = {10210},
  pages     = {260--289},
  year      = {2017},
  note = "DOI: 10.1007/978-3-319-56620-7\_10"
}

@article{avigad-harrison-2014,
  author    = {Jeremy Avigad and
               John Harrison},
  title     = {Formally verified mathematics},
  journal   = {Communications of the {ACM}},
  volume    = {57},
  number    = {4},
  pages     = {66--75},
  year      = {2014}
}

@inproceedings{beringer-et-al-2015,
  author    = {Lennart Beringer and
               Adam Petcher and
               Katherine Q. Ye and
               Andrew W. Appel},
  editor    = {Jaeyeon Jung and
               Thorsten Holz},
  title     = {Verified Correctness and Security of {OpenSSL} {HMAC}},
  booktitle = {{USENIX} Security Symposium ({USENIX} Security 15)},
  pages     = {207--221},
  publisher = {{USENIX} Association},
  year      = {2015},
  note = "DOI: 10.1145/3133956.3133974"
}

@article{DBLP:journals/corr/abs-1708-08542,
  author    = {Katherine Q. Ye and
               Matthew Green and
               Naphat Sanguansin and
               Lennart Beringer and
               Adam Petcher and
               Andrew W. Appel},
  title     = {Verified Correctness and Security of {mbedTLS} {HMAC-DRBG}},
  journal   = {CoRR},
  volume    = {abs/1708.08542},
  year      = {2017},
  url       = {http://arxiv.org/abs/1708.08542},
  timestamp = {Tue, 05 Sep 2017 10:03:46 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1708-08542},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@book{neukirch-1999,
  author = {J\"urgen Neukirch},
  title = "Algebraic Number Theory",
  series = "Grundlehren der mathematischen Wissenschaften",
  volume = 322,
  year = 1999,
  publisher = "Springer",
  note = "DOI: 10.1007/978-3-662-03983-0"}

@inproceedings{korovin-2008,
  author    = {Konstantin Korovin},
  editor    = {Alessandro Armando and
               Peter Baumgartner and
               Gilles Dowek},
  title     = {{iProver}---{A}n Instantiation-Based Theorem Prover for First-Order Logic
               (System Description)},
  booktitle = {International Joint Conference on Automated Reasoning ({IJCAR} 2008)},
  series    = {Lecture Notes in Computer Science},
  volume    = {5195},
  pages     = {292--298},
  publisher = {Springer},
  year      = {2008}
}

@article{kaliszyk-urban-2014,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {Learning-Assisted Automated Reasoning with {F}lyspeck},
  journal   = {J. Automated Reasoning},
  volume    = {53},
  number    = {2},
  pages     = {173--213},
  year      = {2014}
}

@article {MR3505181,
    AUTHOR = {Fasel, Jean},
     TITLE = {On the number of generators of ideals in polynomial rings},
  journal = "Ann. Math. II",
    VOLUME = {184},
      YEAR = {2016},
    NUMBER = {1},
     PAGES = {315--331}
}

@article {MR3702676,
    AUTHOR = {Fasel, Jean},
     TITLE = {Erratum on ``{O}n the number of generators of ideals in
              polynomial rings"},
  journal = "Ann. Math. II",
    VOLUME = {186},
      YEAR = {2017},
    NUMBER = {2},
     PAGES = {647--648},
     note = "DOI: 10.4007/annals.2017.186.2.7"
}

@article{blanchette-et-al-2016-types,
  author    = {Jasmin Christian Blanchette and
               Sascha B{\"{o}}hme and
               Andrei Popescu and
               Nicholas Smallbone},
  title     = {Encoding Monomorphic and Polymorphic Types},
  journal   = {Logical Methods in Computer Science},
  volume    = {12},
  number    = {4},
  year      = {2016},
  note = "DOI: 10.2168/LMCS-12(4:13)2016"
}

@article{duran-et-al-2014,
  title = "The Misfortunes of a Trio of Mathematicians Using Computer Algebra
    Systems. {C}an We Trust in Them?",
  author = "Antonio J. Durán and Mario Pérez and Juan L. Varona",
  journal = "Notices of the AMS",
  volume = 61,
  number = 10,
  pages = "1249--1252",
  year = 2014,
  note = "DOI: 10.1090/noti1173"}

@inproceedings{dahmen-et-al-2019,
  author    = {Sander R. Dahmen and
               Johannes H{\"{o}}lzl and
               Robert Y. Lewis},
  editor    = {John Harrison and
               John O'Leary and
               Andrew Tolmach},
  title     = {Formalizing the Solution to the Cap Set Problem},
  booktitle = {Interactive Theorem Proving ({ITP} 2019)},
  series    = {LIPIcs},
  volume    = {141},
  pages     = {15:1--15:19},
  publisher = {Schloss Dagstuhl---Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2019},
  XXXurl       = {https://doi.org/10.4230/LIPIcs.ITP.2019.15},
  note       = {DOI: 10.4230/LIPIcs.ITP.2019.15},
}

@article{bordg-et-al-2022,
author = {Anthony Bordg and Lawrence Paulson and Wenda Li},
title = {Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types},
journal = {Experimental Mathematics},
volume = {31},
number = {2},
pages = {364--382},
year  = {2022},
publisher = {Taylor & Francis},
doi = {10.1080/10586458.2022.2062073},
URL = {https://doi.org/10.1080/10586458.2022.2062073},
eprint = {https://doi.org/10.1080/10586458.2022.2062073},
note = {DOI: 10.1080/10586458.2022.2062073},
}

@article{eberl-2019,
  author    = {Manuel Eberl},
  title     = {The Irrationality of {\(\zeta\)}(3)},
  journal   = {Arch. Formal Proofs},
  volume    = {2019},
  year      = {2019},
  url       = {https://www.isa-afp.org/entries/Zeta\_3\_Irrational.html},
  timestamp = {Mon, 25 May 2020 09:13:18 +0200},
  biburl    = {https://dblp.org/rec/journals/afp/Eberl19c.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
}

@article{mahboubi-sibut-pinote-2021,
  author    = {Assia Mahboubi and
               Thomas Sibut{-}Pinote},
  title     = {A Formal Proof of the Irrationality of {\(\zeta\)}(3)},
  journal   = {Logical Methods in Computer Science},
  volume    = {17},
  number    = {1},
  year      = {2021},
  XXXurl       = {https://lmcs.episciences.org/7193},
  note = "DOI: 10.23638/LMCS-17(1:16)2021"
}

@inproceedings{buzzard-et-al-2020,
  author    = {Kevin Buzzard and
               Johan Commelin and
               Patrick Massot},
  editor    = {Jasmin Blanchette and
               Cătălin Hrițcu},
  title     = {Formalising perfectoid spaces},
  booktitle = {Certified Programs and Proofs ({CPP} 2020)},
  pages     = {299--312},
  publisher = {{ACM}},
  year      = {2020},
  url       = {https://doi.org/10.1145/3372885.3373830},
  note       = {DOI: 10.1145/3372885.3373830},
}

@article{castelvecchi-2021-lte,
  author = "Davide Castelvecchi",
  title = "Mathematicians welcome computer-assisted proof in `grand unification' theory",
  journal = "Nature",
  XXXdate = "18 June 2021",
  XXXurl = "https://www.nature.com/articles/d41586-021-01627-2",
  year = 2021,
  volume = 595,
  pages = "18--19",
  note = "DOI: 10.1038/d41586-021-01627-2"
}

%%% TODO: Update
@article{lewis-wu-2022,
  author = "Lewis, Robert Y. and Wu, Minchao",
  title = "A Bi-Directional Extensible Interface Between {L}ean and {M}athematica",
  journal = "Journal of Automated Reasoning",
  year = "2022 (online first)",
  note = "DOI: 10.1007/s10817-021-09611-1"}

@article{kaliszyk-urban-2015-holy,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {{HOL(y)Hammer}: Online {ATP} Service for {HOL} {L}ight},
  journal   = {Math. Comput. Sci.},
  volume    = {9},
  number    = {1},
  pages     = {5--22},
  year      = {2015}
}

@article{urban-et-al-2013,
  author    = {Josef Urban and
               Piotr Rudnicki and
               Geoff Sutcliffe},
  title     = {{ATP} and Presentation Service for {M}izar Formalizations},
  journal   = {J. Autom. Reason.},
  volume    = {50},
  number    = {2},
  pages     = {229--241},
  year      = {2013}
}

@article{czajka-kaliszyk-2018,
  author    = {{\L}ukasz Czajka and Cezary Kaliszyk},
  title     = {Hammer for {C}oq: Automation for Dependent Type Theory},
  journal   = {Journal of Automated Reasoning},
  volume    = {61},
  number    = {1--4},
  pages     = {423--453},
  year      = {2018},
  note = "DOI: 10.1007/s10817-018-9458-4"
}

@article{bachmair-ganzinger-1994,
  author    = {Leo Bachmair and
               Harald Ganzinger},
  title     = {Rewrite-Based Equational Theorem Proving with Selection and Simplification},
  journal   = {Journal of Logic and Computation},
  volume    = {4},
  number    = {3},
  pages     = {217--247},
  year      = {1994},
  note = "DOI: 10.1093/logcom/4.3.217"
}

@inproceedings{vukmirovic-et-al-2021-making,
  author={Petar Vukmirovi\'c and Alexander Bentkamp and Jasmin Blanchette and Simon Cruanes and Visa Nummelin and Sophie Tourret},
  editor    = {Andr\'e Platzer and Geoff Sutcliffe},
  title={Making Higher-Order Superposition Work},
  booktitle = {Conference on Automated Deduction (CADE-28)},
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer},
  year      = {2021},
  volume    = {12699},
  pages     = {415--432},
  note = "DOI: 10.1007/978-3-030-79876-5\_24"
}

@inproceedings{bentkamp-et-al-2021-hosup,
  title={Superposition for full higher-order logic},
  author={Alexander Bentkamp and Jasmin Blanchette and Sophie Tourret and Petar Vukmirovi\'c},
  editor = "Andr\'e Platzer and Geoff Sutcliffe",
  booktitle = {Conference on Automated Deduction (CADE-28)},
  year = 2021,
  series = "Lecture Notes in Computer Science",
  volume = "12699",
  pages = "396--412",
  publisher = "Springer",
  note = "DOI: 10.1007/978-3-030-79876-5\_23"}

@inproceedings{baanen-et-al-2021,
  author    = {Anne Baanen and
               Sander R. Dahmen and
               Ashvni Narayanan and
               Filippo A. E. Nuccio Mortarino Majno di Capriglio},
  editor    = {Liron Cohen and
               Cezary Kaliszyk},
  title     = {A Formalization of {D}edekind Domains and Class Groups of Global Fields},
  booktitle = "Interactive Theorem Proving (ITP 2021\/)",
  series    = {LIPIcs},
  volume    = {193},
  pages     = {5:1--5:19},
  publisher = {Schloss Dagstuhl---Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2021},
  url       = {https://doi.org/10.4230/LIPIcs.ITP.2021.5},
  note       = {DOI: 10.4230/LIPIcs.ITP.2021.5},
}

@book{cohen-1993,
  author = {Henri Cohen},
  title = "A Course in Computational Algebraic Number Theory",
  series = "Graduate Texts in Mathematics",
  volume = 138,
  year = 1993,
  publisher = "Springer",
  note = "DOI: 10.1007/978-3-662-02945-9"}

@inproceedings{limperg-from-2023,
  author    = {Jannis Limperg and
               Asta Halkj{\ae}r From},
  editor    = {Robbert Krebbers and
               Dmitriy Traytel and
               Brigitte Pientka and
               Steve Zdancewic},
  title     = {{A}esop: White-Box Best-First Proof Search for {L}ean},
  booktitle = {Certified Programs and Proofs ({CPP} 2023)},
  pages     = {253--266},
  publisher = {{ACM}},
  year      = {2023},
  url       = {https://doi.org/10.1145/3573105.3575671},
  note      = {DOI: 10.1145/3573105.3575671},
  timestamp = {Fri, 13 Jan 2023 13:05:42 +0100},
  biburl    = {https://dblp.org/rec/conf/cpp/LimpergF23.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{mathlib-mathlib-2020,
  title = "The {L}ean Mathematical Library",
  author = "\mathlibcommunity",
  editor = "Jasmin Blanchette and C\u{a}t\u{a}lin Hri\cb{t}cu",
  booktitle = "Certified Programs and Proofs (CPP 2020)",
  publisher = "ACM",
  pages = "367--381",
  year = 2020,
  note          = {DOI: 10.1145/3372885.3373824},
  XXXnote = {\url{https://arxiv.org/pdf/1910.09336.pdf}}}

@article{blanchette-et-al-2016,
  author    = {Jasmin C. Blanchette and
               Cezary Kaliszyk and
               Lawrence C. Paulson and
               Josef Urban},
  title     = {Hammering towards {QED}},
  journal   = {Journal of Formalized Reasoning},
  volume    = {9},
  number    = {1},
  pages     = {101--148},
  year      = {2016},
  XXXurl       = {https://doi.org/10.6092/issn.1972-5787/4593},
  note       = {DOI: 10.6092/issn.1972-5787/4593},
}

@inproceedings{czajka-et-al-2018,
  author       = {Lukasz Czajka and
                  Burak Ekici and
                  Cezary Kaliszyk},
  editor       = {Florian Rabe and
                  William M. Farmer and
                  Grant O. Passmore and
                  Abdou Youssef},
  title        = {Concrete Semantics with {C}oq and {CoqHammer}},
  booktitle    = {Conference on Intelligent Computer Mathematics ({CICM} 2018)},
  series       = {Lecture Notes in Computer Science},
  volume       = {11006},
  pages        = {53--59},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-96812-4\_5},
  note = {DOI: 10.1007/978-3-319-96812-4\_5},
  timestamp    = {Wed, 16 Mar 2022 23:55:39 +0100},
  biburl       = {https://dblp.org/rec/conf/mkm/CzajkaEK18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{barbosa-et-al-2019,
author	= {Haniel Barbosa and Andrew Reynolds and Daniel El Ouraoui and Cesare Tinelli and Clark W. Barrett},
editor	= {Pascal Fontaine},
title	= {Extending {SMT} solvers to higher-order logic},
booktitle	= {Conference on Automated Deduction ({CADE}-27)},
series	= {Lecture Notes in Computer Science},
volume	= {11716},
pages	= {35--54},
publisher	= {Springer},
year	= {2019},
note = {DOI: 10.1007/978-3-030-29436-6\_3}
}

@inproceedings{vukmirovic-et-al-2023,
  title = "Extending a high-performance prover to higher-order logic",
  author = "Petar Vukmirovi\'c and Jasmin Blanchette and Stephan Schulz",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems {\upshape(}TACAS 2023\/{\upshape)}",
  editor = "Natasha Sharygina and Sriram Sankaranarayanan",
  series = "Lecture Notes in Computer Science",
  volume       = {13994},
  pages        = {111--129},
  publisher = "Springer",
  note = "DOI: 10.1007/978-3-031-30820-8\_10",
  year = 2023}

@article{sb-21-leo3,
author	= {Alexander Steen and Christoph Benzm{\"{u}}ller},
title	= {Extensional Higher-Order Paramodulation in {Leo-III}},
journal	= {Journal of Automated Reasoning},
volume	= {65},
number	= {6},
pages	= {775--807},
year	= {2021},
xxxurlXXX	= {https://doi.org/10.1007/s10817-021-09588-x},
note	= {DOI: 10.1007/s10817-021-09588-x},
xxxtimestamp	= {Tue, 13 Jul 2021 13:26:51 +0200},
xxxbiburlXXX	= {https://dblp.org/rec/journals/jar/SteenB21.bib},
xxxbibsource	= {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{br-20-vampire-ho-combs,
author	= {Ahmed Bhayat and Giles Reger},
title	= {A Combinator-Based Superposition Calculus for Higher-Order Logic},
editor	= {Nicolas Peltier and Viorica Sofronie{-}Stokkermans},
booktitle	= {International Joint Conference on Automated Reasoning ({IJCAR} 2020) {(1)}},
series	= {Lecture Notes in Computer Science},
volume	= {12166},
pages	= {278--296},
publisher	= {Springer},
year	= {2020},
note = "DOI: 10.1007/978-3-030-51074-9\_16"
}

@inproceedings{boyer-moore-1973,
  author       = {Robert S. Boyer and
                  J. Strother Moore},
  editor       = {Nils J. Nilsson},
  title        = {Proving Theorems about {LISP} Functions},
  booktitle    = {IJCAI 1973},
  pages        = {486--493},
  publisher    = {William Kaufmann},
  year         = {1973},
  XXXurl          = {http://ijcai.org/Proceedings/73/Papers/053.pdf},
  url = {https://doi.org/10.1145/321864.321875},
  note = {DOI: 10.1145/321864.321875},
}

@inproceedings{hajdu-et-al-2022,
  author       = {M{\'{a}}rton Hajd{\'{u}} and
                  Petra Hozzov{\'{a}} and
                  Laura Kov{\'{a}}cs and
                  Giles Reger and
                  Andrei Voronkov},
  editor       = {Jean{-}Fran{\c{c}}ois Raskin and
                  Krishnendu Chatterjee and
                  Laurent Doyen and
                  Rupak Majumdar},
  title        = {Getting Saturated with Induction},
  booktitle    = {Principles of Systems Design---Essays Dedicated to Thomas A. Henzinger
                  on the Occasion of His 60th Birthday},
  series       = {Lecture Notes in Computer Science},
  volume       = {13660},
  pages        = {306--322},
  publisher    = {Springer},
  year         = {2022},
  XXXurl          = {https://doi.org/10.1007/978-3-031-22337-2\_15},
  XXXdoi          = {10.1007/978-3-031-22337-2\_15},
  note = {DOI: 10.1007/978-3-031-22337-2\_15},
}

@inproceedings{hozzova-et-al-2021,
  author       = {Petra Hozzov{\'{a}} and
                  Laura Kov{\'{a}}cs and
                  Andrei Voronkov},
  editor       = {Andr{\'{e}} Platzer and
                  Geoff Sutcliffe},
  title        = {Integer Induction in Saturation},
  booktitle    = {{CADE}-28},
  series       = {Lecture Notes in Computer Science},
  volume       = {12699},
  pages        = {361--377},
  publisher    = {Springer},
  year         = {2021},
  XXXurl          = {https://doi.org/10.1007/978-3-030-79876-5\_21},
  XXXdoi          = {10.1007/978-3-030-79876-5\_21},
  note = {DOI: 10.1007/978-3-030-79876-5\_21},
}

@inproceedings{baanen-et-al-2023,
  author = {Baanen, Anne and Best, Alex J. and Coppola, Nirvana and Dahmen, Sander R.},
  title = {Formalized Class Group Computations and Integral Points on {M}ordell Elliptic Curves},
  year = {2023},
  isbn = {9798400700262},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3573105.3575682},
  note = {DOI: 10.1145/3573105.3575682},
  booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  pages = {47--62}, numpages = {16},
  keywords = {Mathlib, algebraic number the- ory, Lean, tactics, Diophantine equations, formalized mathematics},
  location = {Boston, MA, USA}, series = {CPP 2023}
}


@article{Bennett-et-al-2015,
title = "Generalized {F}ermat equations: A miscellany",
author = "Michael A. Bennett and Imin Chen and Sander R. Dahmen and Soroosh Yazdani",
year = "2015",
doi = "10.1142/S179304211530001X",
language = "English",
volume = "11",
pages = "1--28",
journal = "International Journal of Number Theory",
issn = "1793-0421",
publisher = "World Scientific Publishing Co. Pte Ltd",
number = "1",
note = {DOI: 10.1142/S179304211530001X},
}

@article{Dahmen-Siksek-2014,
title = "Perfect powers expressible as sums of two fifth or seventh powers",
author = "Sander R. Dahmen and Samir Siksek",
year = "2014",
doi = "10.4064/aa164-1-5",
language = "English",
volume = "164",
pages = "65--100",
journal = "Acta Arithmetica",
issn = "0065-1036",
publisher = "Instytut Matematyczny",
number = "1",
note = {DOI: 10.4064/aa164-1-5},
}

@article{Bennett-Dahmen-2013,
    AUTHOR = {Bennett, Michael A. and Dahmen, Sander R.},
     TITLE = {Klein forms and the generalized superelliptic equation},
  JOURNAL = {Annals of Mathematics, Second Series},
    VOLUME = {177},
      YEAR = {2013},
    NUMBER = {1},
     PAGES = {171--239},
      ISSN = {0003-486X},
   MRCLASS = {11G05},
  MRNUMBER = {2999040},
MRREVIEWER = {Byoung Du Kim},
       DOI = {10.4007/annals.2013.177.1.4},
       URL = {https://doi.org/10.4007/annals.2013.177.1.4},
       note = {DOI: 10.4007/annals.2013.177.1.4},
}

@article {vLangen2021,
    AUTHOR = {van Langen, Joey M.},
     TITLE = {On the sum of fourth powers in arithmetic progression},
  JOURNAL = {International Journal of Number Theory},
    VOLUME = {17},
      YEAR = {2021},
    NUMBER = {1},
     PAGES = {191--221},
      ISSN = {1793-0421},
   MRCLASS = {11D61 (11D41 11F11 11F80)},
  MRNUMBER = {4206931},
MRREVIEWER = {Volker Ziegler},
       DOI = {10.1142/S1793042121500093},
       URL = {https://doi.org/10.1142/S1793042121500093},
      note = {DOI: 10.1142/S1793042121500093},
}

@phdthesis{vLangen2022,
title = "Automating the modular method for Q-curves to solve Diophantine equations",
keywords = "Diophantische vergelijkingen, Modulaire methode, Frey krommes, Q-krommes, Diophantie equations, Modular method, Frey curves, Q-curves",
author = "{van Langen}, {Joey Matthias}",
year = "2022",
month = jan,
day = "27",
language = "English",
school = "Vrije Universiteit Amsterdam",
URL = {https://research.vu.nl/en/publications/automating-the-modular-method-for-q-curves-to-solve-diophantine-e},
 note = {\url{https://research.vu.nl/en/publications/automating-the-modular-method-for-q-curves-to-solve-diophantine-e}},
}

@article{buzzard-et-al-2022,
author = {Kevin Buzzard and Chris Hughes and Kenny Lau and Amelia Livingston and Ramon Fernández Mir and Scott Morrison},
title = {Schemes in {L}ean},
journal = {Experimental Mathematics},
volume = {31},
number = {2},
pages = {355--363},
year  = {2022},
publisher = {Taylor & Francis},
doi = {10.1080/10586458.2021.1983489},
URL = { https://doi.org/10.1080/10586458.2021.1983489},
eprint = {https://doi.org/10.1080/10586458.2021.1983489},
note = {DOI: 10.1080/10586458.2021.1983489},
}

@article {Xu-Ye-2023,
    AUTHOR = {Xu, Xingwang and Ye, Jian},
     TITLE = {Retracted article: {C}losed three-dimensional vacuum static
              spaces},
  JOURNAL = {Inventiones Mathematicae},
    VOLUME = {231},
      YEAR = {2023},
    NUMBER = {3},
     PAGES = {1541--1542},
      ISSN = {0020-9910},
   MRCLASS = {53C50},
  MRNUMBER = {4549093},
       DOI = {10.1007/s00222-022-01139-4},
       URL = {https://doi.org/10.1007/s00222-022-01139-4},
       note = {DOI: 10.1007/s00222-022-01139-4},
}

@misc{LTE,
  title = {Liquid Tensor Experiment},
  howpublished = {\url{https://github.com/leanprover-community/lean-liquid}},
  note = {Version: 2022-10-14},
}

@misc{PFR,
  title = {The Polynomial {F}reiman-{R}uzsa Conjecture},
  howpublished = {\url{https://github.com/teorth/pfr}},
  note = {Version: 2024-07-02},
}

@misc{FLT,
  title = {Fermat's Last Theorem},
  howpublished = {\url{https://github.com/ImperialCollegeLondon/FLT}},
  note = {Version: 2024-06-20},
}

@book{cohen-2007-I,
     AUTHOR = {Cohen, Henri},
     TITLE = {Number theory. {V}ol. {I}. {T}ools and {D}iophantine
              equations},
    SERIES = {Graduate Texts in Mathematics},
    VOLUME = {239},
 PUBLISHER = {Springer, New York},
      YEAR = {2007},
     PAGES = {xxiv+650},
      ISBN = {978-0-387-49922-2},
   MRCLASS = {11-01 (11Dxx 11Rxx 11Sxx)},
  MRNUMBER = {2312337},
MRREVIEWER = {R.\ C.\ Baker},
url = {https://doi.org/10.1007/978-0-387-49923-9},
note ={DOI: 10.1007/978-0-387-49923-9},
}

@book {cohen-2007-II,
    AUTHOR = {Cohen, Henri},
     TITLE = {Number theory. {V}ol. {II}. {A}nalytic and modern tools},
    SERIES = {Graduate Texts in Mathematics},
    VOLUME = {240},
 PUBLISHER = {Springer, New York},
      YEAR = {2007},
     PAGES = {xxiv+596},
      ISBN = {978-0-387-49893-5},
   MRCLASS = {11-01 (11D61 11F80 11J86 11Mxx)},
  MRNUMBER = {2312338},
MRREVIEWER = {R.\ C.\ Baker},
url = {https://doi.org/10.1007/978-0-387-49894-2},
note = {DOI: 10.1007/978-0-387-49894-2},
}

@book{smart-1998,
    AUTHOR = {Smart, Nigel P.},
     TITLE = {The algorithmic resolution of {D}iophantine equations},
    SERIES = {London Mathematical Society Student Texts},
    VOLUME = {41},
 PUBLISHER = {Cambridge University Press, Cambridge},
      YEAR = {1998},
     PAGES = {xvi+243},
      ISBN = {0-521-64633-2},
   MRCLASS = {11Y50 (11Dxx 11J70 11J86)},
  MRNUMBER = {1689189},
MRREVIEWER = {Yuri\ Bilu},
       DOI = {10.1017/CBO9781107359994},
       URL = {https://doi.org/10.1017/CBO9781107359994},
       note = {DOI: 10.1017/CBO9781107359994},
}

@inproceedings{de-moura-ullrich-2021,
  author       = {Leonardo de Moura and
                  Sebastian Ullrich},
  editor       = {Andr{\'{e}} Platzer and
                  Geoff Sutcliffe},
  title        = {The {Lean} 4 Theorem Prover and Programming Language},
  booktitle    = {Conference on Automated Deduction (CADE-28)},
  series       = {Lecture Notes in Computer Science},
  volume       = {12699},
  pages        = {625--635},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-79876-5\_37},
  note          = {DOI: 10.1007/978-3-030-79876-5\_37},
  XXXtimestamp    = {Thu, 29 Sep 2022 08:36:56 +0200},
  XXXbiburl       = {https://dblp.org/rec/conf/cade/Moura021.bib},
  XXXbibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{Dahmen-vLangen,
author = {Sander R. Dahmen and Joey M. van Langen},
title = {Explicitly determining perfect powers in several elliptic divisibility sequences},
journal = {Preprint},
year = {2023},
[ages = {23 pp.},
note = {\url{https://arxiv.org/pdf/2310.13244}. DOI: 10.48550/arXiv.2310.13244},
}

@article {BCDDF-2023,
    AUTHOR = {Billerey, Nicolas and Chen, Imin and Demb\'el\'e, Lassina and
              Dieulefait, Luis and Freitas, Nuno},
     TITLE = {Some extensions of the modular method and {F}ermat equations
              of signature {$(13,13,n)$}},
   XJOURNAL = {Publ. Mat.},
  JOURNAL = {Publicacions Matem\`atiques},
    VOLUME = {67},
      YEAR = {2023},
    NUMBER = {2},
     PAGES = {715--741},
      ISSN = {0214-1493,2014-4350},
   MRCLASS = {11D41 (11F80 11G10)},
  MRNUMBER = {4609017},
MRREVIEWER = {Ariel\ M.\ Pacetti},
       DOI = {10.5565/publmat6722309},
       URL = {https://doi.org/10.5565/publmat6722309},
       note = {DOI: 10.5565/publmat6722309},
}

@article {Bilu-Hanrot-1996,
    AUTHOR = {Bilu, Yuri and Hanrot, Guillaume},
     TITLE = {Solving {T}hue equations of high degree},
  JOURNAL = {Journal of Number Theory},
    VOLUME = {60},
      YEAR = {1996},
    NUMBER = {2},
     PAGES = {373--392},
      ISSN = {0022-314X,1096-1658},
   MRCLASS = {11D41},
  MRNUMBER = {1412969},
MRREVIEWER = {T.\ N.\ Shorey},
       DOI = {10.1006/jnth.1996.0129},
       URL = {https://doi.org/10.1006/jnth.1996.0129},
       note = {DOI: 10.1006/jnth.1996.0129},
}

@inproceedings{schulz-et-al-2019,
  author       = {Stephan Schulz and
                  Simon Cruanes and
                  Petar Vukmirovic},
  editor       = {Pascal Fontaine},
  title        = {Faster, Higher, Stronger: {E} 2.3},
  booktitle    = {CADE 2019},
  series       = {Lecture Notes in Computer Science},
  volume       = {11716},
  pages        = {495--507},
  publisher    = {Springer},
  year         = {2019},
  url          = {https://doi.org/10.1007/978-3-030-29436-6\_29},
  note          = {DOI: 10.1007/978-3-030-29436-6\_29},
}

@inproceedings{kovacs-voronkov-2013,
  author       = {Laura Kov{\'{a}}cs and
                  Andrei Voronkov},
  editor       = {Natasha Sharygina and
                  Helmut Veith},
  title        = {First-Order Theorem Proving and Vampire},
  booktitle    = {{CAV} 2013},
  series       = {Lecture Notes in Computer Science},
  volume       = {8044},
  pages        = {1--35},
  publisher    = {Springer},
  year         = {2013},
  url          = {https://doi.org/10.1007/978-3-642-39799-8\_1},
  note         = {DOI: 10.1007/978-3-642-39799-8\_1},
}

@article{Tzanakis-deWeger-1992,
author = {Nikolaos Tzanakis and Benne M. M. de Weger},
journal = {Compositio Mathematica},
keywords = {algorithm; Thue-Mahler equation},
language = {eng},
number = {3},
pages = {223--288},
publisher = {Kluwer Academic Publishers},
title = {How to explicitly solve a {T}hue-{M}ahler equation},
note = {\url{http://eudml.org/doc/90185}},
volume = {84},
year = {1992},
}

@InProceedings{Angdinata-XU-2023,
  author =	{Angdinata, David Kurniadi and Xu, Junyan},
  title =	{{An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.6},
  URN =		{urn:nbn:de:0030-drops-183817},
  doi =		{10.4230/LIPIcs.ITP.2023.6},
  annote =	{Keywords: formal math, algebraic geometry, elliptic curve, group law, Lean, mathlib},
  note = {DOI: 10.4230/LIPIcs.ITP.2023.6},
}

@InProceedings{Best-et-al-2023,
  author =	{Best, Alex J. and Birkbeck, Christopher and Brasca, Riccardo and Rodriguez Boidi, Eric},
  title =	{{Fermat’s Last Theorem for Regular Primes}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{36:1--36:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.36},
  URN =		{urn:nbn:de:0030-drops-184115},
  doi =		{10.4230/LIPIcs.ITP.2023.36},
  annote =	{Keywords: Fermat’s Last Theorem, Cyclotomic fields, Interactive theorem proving, Lean},
  note = {DOI: 10.4230/LIPIcs.ITP.2023.36},
}


@manual{sagemath,
  Key          = {SageMath},
  Author       = {{The Sage Developers}},
  Title        = {{S}ageMath, the {S}age {M}athematics {S}oftware {S}ystem ({V}ersion 10.3)},
  note         = {\url{https://www.sagemath.org}. DOI: 10.5281/zenodo.10841614},
  Year         = {2024},
}

@inproceedings{barbosa-et-al-2022-cvc5,
  author       = {Haniel Barbosa and
                  Clark W. Barrett and
                  Martin Brain and
                  Gereon Kremer and
                  Hanna Lachnitt and
                  Makai Mann and
                  Abdalrhman Mohamed and
                  Mudathir Mohamed and
                  Aina Niemetz and
                  Andres N{\"{o}}tzli and
                  Alex Ozdemir and
                  Mathias Preiner and
                  Andrew Reynolds and
                  Ying Sheng and
                  Cesare Tinelli and
                  Yoni Zohar},
  editor       = {Dana Fisman and
                  Grigore Rosu},
  title        = {{cvc5}: {A} Versatile and Industrial-Strength {SMT} Solver},
  booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems
                  - 28th International Conference, {TACAS} 2022, Held as Part of the
                  European Joint Conferences on Theory and Practice of Software, {ETAPS}
                  2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {I}},
  series       = {Lecture Notes in Computer Science},
  volume       = {13243},
  pages        = {415--442},
  publisher    = {Springer},
  year         = {2022},
  url          = {https://doi.org/10.1007/978-3-030-99524-9\_24},
  doi          = {10.1007/978-3-030-99524-9\_24},
  timestamp    = {Fri, 29 Apr 2022 14:50:36 +0200},
  biburl       = {https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org},
  note = {DOI: 10.1007/978-3-030-99524-9\_24},
}

@inproceedings{clune-et-al-2024,
  author    = {Joshua Clune and Yicheng Qian and Alexander Bentkamp and Jeremy Avigad},
  editor    = {Yves Bertot and Temur Kutsia and Michael Norrish},
  title     = {Duper: A Proof Producing Superposition Theorem Prover for Dependent Type Theory},
  booktitle = "Interactive Theorem Proving (ITP 2024\/)",
  series    = {LIPIcs},
  volume    = {309},
  XXXpages     = {5:1--5:19},
  publisher = {Schloss Dagstuhl---Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2024},
  XXXurl       = {https://doi.org/10.4230/LIPIcs.ITP.2021.5},
  XXXnote       = {DOI: 10.4230/LIPIcs.ITP.2021.5},
  note = "To be published"
}

@inproceedings{zhan-2016,
  author       = {Bohua Zhan},
  editor       = {Jasmin Christian Blanchette and
                  Stephan Merz},
  title        = {{AUTO2}, {A} Saturation-Based Heuristic Prover for Higher-Order Logic},
  booktitle    = {Interactive Theorem Proving ({ITP} 2016)},
  series       = {LNCS},
  volume       = {9807},
  pages        = {441--456},
  publisher    = {Springer},
  year         = {2016},
  XXXurl          = {https://doi.org/10.1007/978-3-319-43144-4\_27},
  XXXdoi          = {10.1007/978-3-319-43144-4\_27},
  note = {DOI: 10.1007/978-3-319-43144-4\_27},
}
