Quelle manual.bib Sprache: Latech

% BibTeX database for the Isabelle documentation

%publishers
@string{AP="Academic Press"}
@string{CUP="Cambridge University Press"}
@string{IEEE="IEEE Computer Society Press"}
@string{LNCS="Lecture Notes in Computer Science"}
@string{MIT="MIT Press"}
@string{NH="North-Holland"}
@string{Prentice="Prentice-Hall"}
@string{PH="Prentice-Hall"}
@string{Springer="Springer-Verlag"}

%institutions
@string{CUCL="Computer Laboratory, University of Cambridge"}
@string{Edinburgh="Department of Computer Science, University of Edinburgh"}
@string{TUM="Department of Informatics, Technical University of Munich"}

%journals
@string{AI="Artificial Intelligence"}
@string{FAC="Formal Aspects of Computing"}
@string{JAR="Journal of Automated Reasoning"}
@string{JCS="Journal of Computer Security"}
@string{JFP="Journal of Functional Programming"}
@string{JLC="Journal of Logic and Computation"}
@string{JLP="Journal of Logic Programming"}
@string{JSC="Journal of Symbolic Computation"}
@string{JSL="Journal of Symbolic Logic"}
@string{PROYAL="Proceedings of the Royal Society of London"}
@string{SIGPLAN="{SIGPLAN} Notices"}
@string{TISSEC="ACM Transactions on Information and System Security"}

%conferences
@string{CADE="International Conference on Automated Deduction"}
@string{POPL="Symposium on Principles of Programming Languages"}
@string{TYPES="Types for Proofs and Programs"}

%A

@incollection{abramsky90,
  author = {Samson Abramsky},
  title  = {The Lazy Lambda Calculus},
  pages  = {65-116},
  editor = {David A. Turner},
  booktitle = {Research Topics in Functional Programming},
  publisher = {Addison-Wesley},
  year  = 1990}

@Unpublished{abrial93,
  author = {J. R. Abrial and G. Laffitte},
  title  = {Towards the Mechanization of the Proofs of Some Classical
    Theorems of Set Theory},
  note  = {preprint},
  year  = 1993,
  month  = Feb}

@incollection{aczel77,
  author = {Peter Aczel},
  title  = {An Introduction to Inductive Definitions},
  pages  = {739-782},
  crossref = {barwise-handbk}}

@Book{aczel88,
  author = {Peter Aczel},
  title  = {Non-Well-Founded Sets},
  publisher = {CSLI},
  year  = 1988}

@inproceedings{Aehlig-Haftmann-Nipkow:2008:nbe,
  author =      {Klaus Aehlig and Florian Haftmann and Tobias Nipkow},
  title =       {A Compiled Implementation of Normalization by Evaluation},
  booktitle =   {TPHOLs '08: Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics},
  year =        {2008},
  isbn =        {978-3-540-71065-3},
  pages =       {352--367},
  publisher =   Springer,
  series =      LNCS,
  volume =      {5170},
  editor =      {Otmane A\"{\i}t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar}
}

@InProceedings{alf,
  author = {Lena Magnusson and Bengt {Nordstr\"{o}m}},
  title  = {The {ALF} Proof Editor and Its Proof Engine},
  crossref = {types93},
  pages  = {213-237}}

@inproceedings{andersson-1993,
  author = "Arne Andersson",
  title = "Balanced Search Trees Made Simple",
  editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides",
  booktitle = "WADS 1993",
  series = LNCS,
  volume = {709},
  pages = "61--70",
  year = 1993,
  publisher = Springer}

@book{andrews86,
  author = "Peter Andrews",
  title  = "An Introduction to Mathematical Logic and Type Theory: to Truth
through Proof",
  publisher = AP,
  series = "Computer Science and Applied Mathematics",
  year  = 1986}

@InProceedings{Aspinall:2000:eProof,
  author =   {David Aspinall},
  title =   {Protocols for Interactive {e-Proof}},
  booktitle =   {Theorem Proving in Higher Order Logics (TPHOLs)},
  year =  2000,
  note =  {Unpublished work-in-progress paper,
                  \url{http://homepages.inf.ed.ac.uk/da/papers/drafts/eproof.ps.gz}}
}

@InProceedings{Aspinall:TACAS:2000,
  author =   {David Aspinall},
  title =   {{P}roof {G}eneral: A Generic Tool for Proof Development},
  booktitle =   {Tools and Algorithms for the Construction and Analysis of
                  Systems (TACAS)},
  year =  2000,
  publisher = Springer,
  series = LNCS,
  volume = 1785,
  pages = "38--42"
}

@Misc{isamode,
  author =  {David Aspinall},
  title =  {Isamode --- {U}sing {I}sabelle with {E}macs},
  note =  {\url{http://homepages.inf.ed.ac.uk/da/Isamode/}}
}

@Misc{proofgeneral,
  author =  {David Aspinall},
  title =  {{P}roof {G}eneral},
  note =  {\url{http://proofgeneral.inf.ed.ac.uk/}}
}

%B

@inproceedings{backes-brown-2010,
  title = "Analytic Tableaux for Higher-Order Logic with Choice",
  author = "Julian Backes and Chad E. Brown",
  booktitle={Automated Reasoning: IJCAR 2010},
  editor={J. Giesl and R. H\"ahnle},
  publisher = Springer,
  series = LNCS,
  volume = 6173,
  pages = "76--90",
  year = 2010}

@book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow},
title="Term Rewriting and All That",publisher=CUP,year=1998}

@manual{isabelle-locale,
  author        = {Clemens Ballarin},
  title         = {Tutorial to Locales and Locale Interpretation},
  institution   = TUM,
  note          = {\url{https://isabelle.in.tum.de/doc/locales.pdf}}
}

@article{Ballarin2014,
  author = {Ballarin, Clemens},
  journal = JAR,
  publisher = Springer,
  title = {Locales: A Module System for Mathematical Theories},
  volume = 52,
  number = 2,
  pages = {123--153},
  url = {https://doi.org/10.1007/s10817-013-9284-7},
  year = {2014}}

@InCollection{Barendregt-Geuvers:2001,
  author =   {H. Barendregt and H. Geuvers},
  title =   {Proof Assistants using Dependent Type Systems},
  booktitle =   {Handbook of Automated Reasoning},
  publisher =  {Elsevier},
  year =  2001,
  editor =  {A. Robinson and A. Voronkov}
}

@inproceedings{barbosa-et-al-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: TACAS 2022 (I)",
  series    = {Lecture Notes in Computer Science},
  volume    = {13243},
  pages     = {415--442},
  publisher = {Springer},
  year      = {2022},
  XXXurl       = {https://doi.org/10.1007/978-3-030-99524-9\_24},
  XXXdoi       = {10.1007/978-3-030-99524-9\_24},
}

@inproceedings{cvc3,
  author    = {Clark Barrett and Cesare Tinelli},
  title     = {{CVC3}},
  booktitle = {CAV},
  editor    = {Werner Damm and Holger Hermanns},
  volume    = {4590},
  series    = LNCS,
  pages     = {298--302},
  publisher = {Springer},
  year      = {2007}
}

@inproceedings{cvc4,
  author    = {Clark Barrett and
               Christopher L. Conway and
               Morgan Deters and
               Liana Hadarean and
               Dejan Jovanovic and
               Tim King and
               Andrew Reynolds and
               Cesare Tinelli},
  title     = {{CVC4}},
  booktitle = {CAV 2011},
  pages     = {171--177},
  editor    = {Ganesh Gopalakrishnan and
               Shaz Qadeer},
  publisher = {Springer},
  series    = LNCS,
  volume    = {6806},
  year      = {2011}
}

@incollection{basin91,
  author = {David Basin and Matt Kaufmann},
  title  = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
     Comparison},
  crossref = {huet-plotkin91},
  pages  = {89-119}}

@Unpublished{HOL-Library,
  author =       {Gertrud Bauer and Tobias Nipkow and Oheimb, David von and
                  Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and
                  Markus Wenzel},
  title =        {The Supplemental {Isabelle/HOL} Library},
  note =         {Part of the Isabelle distribution,
                  \url{https://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
  year =         2002
}

@InProceedings{Bauer-Wenzel:2000:HB,
  author =   {Gertrud Bauer and Markus Wenzel},
  title =   {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
      {I}sabelle/{I}sar},
  booktitle =   {Types for Proofs and Programs: TYPES'99},
  editor =       {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m
                  and Jan Smith},
  series =  {LNCS},
  year =  2000
}

@InProceedings{Bauer-Wenzel:2001,
  author =       {Gertrud Bauer and Markus Wenzel},
  title =        {Calculational reasoning revisited --- an {Isabelle/Isar} experience},
  crossref =     {tphols2001}}

@inproceedings{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 = "Automated Reasoning: IJCAR 2008",
  publisher = Springer,
  series = LNCS,
  volume = 5195,
  pages = "162--170",
  year = 2008}

@inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL,
    author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
    booktitle = {Theorem Proving in Higher Order Logics},
    pages = {131--146},
    title = {Turning Inductive into Equational Specifications},
    year = {2009}
}

@INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
  crossref        = "tphols2000",
  title           = "Proof terms for simply typed higher order logic",
  author          = "Stefan Berghofer and Tobias Nipkow",
  pages           = "38--52"}

@inproceedings{berghofer-nipkow-2004,
  author = {Stefan Berghofer and Tobias Nipkow},
  title = {Random Testing in {I}sabelle/{HOL}},
  pages = {230--239},
  editor = "J. Cuellar and Z. Liu",
  booktitle = {{SEFM} 2004},
  publisher = IEEE,
  year = 2004}

@InProceedings{Berghofer-Nipkow:2002,
  author =       {Stefan Berghofer and Tobias Nipkow},
  title =        {Executing Higher Order Logic},
  booktitle =    {Types for Proofs and Programs: TYPES'2000},
  editor =       {P. Callaghan and Z. Luo and J. McKinna and R. Pollack},
  series =       LNCS,
  publisher =    Springer,
  volume =       2277,
  year =         2002}

@InProceedings{Berghofer-Wenzel:1999:TPHOL,
  author =   {Stefan Berghofer and Markus Wenzel},
  title =   {Inductive datatypes in {HOL} --- lessons learned in
                  {F}ormal-{L}ogic {E}ngineering},
  crossref =     {tphols99}}

@InProceedings{Bezem-Coquand:2005,
  author =   {M.A. Bezem and T. Coquand},
  title =   {Automating {Coherent Logic}},
  booktitle = {LPAR-12},
  year = 2005,
  editor =   {G. Sutcliffe and A. Voronkov},
  volume =   3835,
  series =   LNCS,
  publisher = Springer}

@manual{isabelle-datatypes,
  author = {Julian Biendarra and Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel},
  title  = {Defining (Co)datatypes and Primitively (Co)recursive Functions in {Isabelle\slash HOL}},
  institution = {TU Munich},
  note          = {\url{https://isabelle.in.tum.de/doc/datatypes.pdf}}}

@book{Bird-Wadler,author="Richard Bird and Philip Wadler",
title="Introduction to Functional Programming",publisher=PH,year=1988}

@book{Bird-Haskell,author="Richard Bird",
title="Introduction to Functional Programming using Haskell",
publisher=PH,year=1998}

@manual{isabelle-nitpick,
  author        = {Jasmin Christian Blanchette},
  title         = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle\slash {HOL}},
  institution   = TUM,
  note          = {\url{https://isabelle.in.tum.de/doc/nitpick.pdf}}
}

@manual{isabelle-sledgehammer,
  author        = {Jasmin Christian Blanchette},
  title         = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle\slash {HOL}},
  institution   = TUM,
  note          = {\url{https://isabelle.in.tum.de/doc/sledgehammer.pdf}}
}

@manual{isabelle-corec,
  author = {Jasmin Christian Blanchette and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel},
  title  = {Defining Nonprimitively Corecursive Functions in {Isabelle\slash HOL}},
  institution = {TU Munich},
  note          = {\url{https://isabelle.in.tum.de/doc/corec.pdf}}}

@inproceedings{blanchette-nipkow-2010,
  title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
  author = "Jasmin Christian Blanchette and Tobias Nipkow",
  crossref = {itp2010}}

@inproceedings{blanchette-et-al-2015-wit,
  author    = {Jasmin Christian Blanchette and
               Andrei Popescu and
               Dmitriy Traytel},
  title     = {Witnessing (Co)datatypes},
  booktitle = {24th European Symposium on Programming, {ESOP} 2015},
  pages     = {359--382},
  year      = {2015},
  editor    = {Jan Vitek},
  series    = {LNCS},
  volume    = {9032},
  publisher = {Springer}
}

@inproceedings{blanchette-et-al-2015-fouco,
  author    = {Jasmin Christian Blanchette and
               Andrei Popescu and
               Dmitriy Traytel},
  title     = {Foundational extensible corecursion: A proof assistant perspective},
  booktitle = {20th {ACM} {SIGPLAN} International Conference on
               Functional Programming, {ICFP} 2015},
  pages     = {192--204},
  year      = {2015},
  editor    = {Kathleen Fisher and
               John H. Reppy},
  publisher = {{ACM}},
}

@misc{blanchette-et-al-201x-amico,
  author    = {Jasmin Christian Blanchette and
               Aymeric Bouzy and
               Andreas Lochbihler and
               Andrei Popescu and
               Dmitriy Traytel},
  title     = {Friends with benefits: Implementing corecursion in foundational proof assistants},
  howpublished = "\url{http://www21.in.tum.de/~blanchet/amico.pdf}",
  year = 2016}

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

@inproceedings{why3,
  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
}

@inproceedings{alt-ergo,
  author = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean and St\'ephane Lescuyer},
  title = {Implementing Polymorphism in {SMT} Solvers},
  booktitle = {SMT '08},
  pages = "1--5",
  publisher = "ACM",
  series = "ICPS",
  year = 2008,
  editor = {Clark Barrett and Leonardo de Moura}}
% /BPR
% and Domagoj Babic and Amit Goel

@inproceedings{boehme-nipkow-2010,
  author={Sascha B\"ohme and Tobias Nipkow},
  title={Sledgehammer: Judgement Day},
  booktitle={Automated Reasoning: IJCAR 2010},
  editor={J. Giesl and R. H\"ahnle},
  publisher=Springer,
  series=LNCS,
  volume = 6173,
  pages = "107--121",
  year=2010}

@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},
  year      = {2009},
  pages     = {151--156},
  editor    = {Renate A. Schmidt},
  booktitle     = {Automated Deduction --- CADE-22},
  series    = {Lecture Notes in Computer Science},
  volume    = {5663},
  publisher = {Springer}
}

@Article{boyer86,
  author = {Robert Boyer and Ewing Lusk and William McCune and Ross
     Overbeek and Mark Stickel and Lawrence Wos},
  title  = {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}
     Axioms},
  journal = JAR,
  year  = 1986,
  volume = 2,
  number = 3,
  pages  = {287-327}}

@book{bm79,
  author = {Robert S. Boyer and J Strother Moore},
  title  = {A Computational Logic},
  publisher = {Academic Press},
  year  = 1979}

@book{bm88book,
  author = {Robert S. Boyer and J Strother Moore},
  title  = {A Computational Logic Handbook},
  publisher = {Academic Press},
  year  = 1988}

@inproceedings{satallax,
  author = "Chad E. Brown",
  title = "Reducing Higher-Order Theorem Proving to a Sequence of {SAT} Problems",
  booktitle = {Automated Deduction --- CADE-23},
  publisher = Springer,
  series = LNCS,
  volume = 6803,
  pages = "147--161",
  editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
  year = 2011}

@Article{debruijn72,
  author = {N. G. de Bruijn},
  title  = {Lambda Calculus Notation with Nameless Dummies,
a Tool for Automatic Formula Manipulation,
with Application to the {Church-Rosser Theorem}},
  journal = {Indag. Math.},
  volume = 34,
  pages  = {381-392},
  year  = 1972}

@InProceedings{bulwahnKN07,
  author   = {Lukas Bulwahn and Alexander Krauss and Tobias Nipkow},
  title    = {Finding Lexicographic Orders for Termination Proofs in {Isabelle/HOL}},
  crossref = {tphols2007},
  pages    = {38--53}
}

@InProceedings{bulwahn-et-al:2008:imperative,
  author   = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
  title    = {Imperative Functional Programming with {Isabelle/HOL}},
  crossref = {tphols2008},
}
%  pages    = {38--53}

@Article{ban89,
  author = {M. Burrows and M. Abadi and R. M. Needham},
  title  = {A Logic of Authentication},
  journal = PROYAL,
  year  = 1989,
  volume = 426,
  pages  = {233-271}}

%C

@PhdThesis{Chaieb-thesis,
  author =       {Amine Chaieb},
  title =        {Automated methods for formal proofs in simple arithmetics and algebra},
  school =       {Technische Universit\"at M\"unchen},
  year =         2008,
  note =      {\url{http://www4.in.tum.de/~chaieb/pubs/pdf/diss.pdf}}}

@InProceedings{Chaieb-Wenzel:2007,
  author =   {Amine Chaieb and Makarius Wenzel},
  title =   {Context aware Calculation and Deduction ---
                  Ring Equalities via {Gr\"obner Bases} in {Isabelle}},
  booktitle =  {Towards Mechanized Mathematical Assistants (CALCULEMUS 2007)},
  editor =  {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
  series =  "LNAI",
  volume =       4573,
  year =  2007,
  publisher =  Springer
}

@TechReport{camilleri92,
  author = {J. Camilleri and T. F. Melham},
  title  = {Reasoning with Inductively Defined Relations in the
   {HOL} Theorem Prover},
  institution = CUCL,
  year  = 1992,
  number = 265,
  month  = Aug}

@Book{charniak80,
  author = {E. Charniak and C. K. Riesbeck and D. V. McDermott},
  title  = {Artificial Intelligence Programming},
  publisher = {Lawrence Erlbaum Associates},
  year  = 1980}

@article{church40,
  author = "Alonzo Church",
  title  = "A Formulation of the Simple Theory of Types",
  journal = JSL,
  year  = 1940,
  volume = 5,
  pages  = "56-68"}

@book{ClarkeGP-book,author="Edmund Clarke and Orna Grumberg and Doron Peled",
title="Model Checking",publisher=MIT,year=1999}

@PhdThesis{coen92,
  author = {Martin D. Coen},
  title  = {Interactive Program Derivation},
  school = {University of Cambridge},
  note  = {Computer Laboratory Technical Report 272},
  month  = nov,
  year  = 1992}

@book{constable86,
  author = {R. L. Constable and others},
  title  = {Implementing Mathematics with the Nuprl Proof
   Development System},
  publisher = Prentice,
  year  = 1986}

@inproceedings{cruanes-2014,
  author = "Simon Cruanes",
  title = "Logtk: A {Logic ToolKit} for Automated Reasoning, and its Implementation",
  booktitle = {4th Workshop on Practical Aspects of Automated Reasoning, PAAR@IJCAR
               2014, Vienna, Austria, 2014},
  year = 2014,
  note =   {Presented at the Practical Aspects of Automated Reasoning (PAAR) workshop}}

%D

@Book{davey-priestley,
  author = {B. A. Davey and H. A. Priestley},
  title  = {Introduction to Lattices and Order},
  publisher = CUP,
  year  = 1990}

@inproceedings{de-moura-2008,
  author    = {Leonardo de Moura and
               Nikolaj Bj{\o}rner},
  editor    = {C. R. Ramakrishnan and
               Jakob Rehof},
  title     = {{Z3}: An Efficient {SMT} Solver},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems --- TACAS 2008},
  series    = {Lecture Notes in Computer Science},
  volume    = {4963},
  pages     = {337--340},
  publisher = {Springer},
  year      = {2008},
  url       = {https://doi.org/10.1007/978-3-540-78800-3\_24},
  doi       = {10.1007/978-3-540-78800-3\_24},
  timestamp = {Tue, 14 May 2019 10:00:53 +0200},
  biburl    = {https://dblp.org/rec/conf/tacas/MouraB08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Book{devlin79,
  author = {Keith J. Devlin},
  title  = {Fundamentals of Contemporary Set Theory},
  publisher = {Springer},
  year  = 1979}

@inproceedings{di-gianantonio-miculan-2003,
  author    = {Di Gianantonio, Pietro and
               Marino Miculan},
  title     = {A Unifying Approach to Recursive and Co-recursive Definitions},
  booktitle = {TYPES 2002},
  year      = {2003},
  pages     = {148--161},
  editor    = {Herman Geuvers and
               Freek Wiedijk},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2646}
}

@book{dummett,
  author = {Michael Dummett},
  title  = {Elements of Intuitionism},
  year  = 1977,
  publisher = {Oxford University Press}}

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

@incollection{dybjer91,
  author = {Peter Dybjer},
  title  = {Inductive Sets and Families in {Martin-L{\"o}f's} Type
    Theory and Their Set-Theoretic Semantics},
  crossref = {huet-plotkin91},
  pages  = {280-306}}

@Article{dyckhoff,
  author = {Roy Dyckhoff},
  title  = {Contraction-Free Sequent Calculi for Intuitionistic Logic},
  journal = JSL,
  year  = 1992,
  volume = 57,
  number = 3,
  pages  = {795-807}}

%F

@Article{IMPS,
  author = {William M. Farmer and Joshua D. Guttman and F. Javier
   Thayer},
  title  = {{IMPS}: An Interactive Mathematical Proof System},
  journal = JAR,
  volume = 11,
  number = 2,
  year  = 1993,
  pages  = {213-248}}

@article{Farmer:2008,
  author    = {William M. Farmer},
  title     = {The seven virtues of simple type theory},
  journal   = {J. Applied Logic},
  volume    = {6},
  number    = {3},
  pages     = {267--286},
  year      = {2008},
  url       = {https://doi.org/10.1016/j.jal.2007.11.001},
}

@inproceedings{felty91a,
  author    = {Amy Felty},
  title     = {A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs},
  booktitle = {Extensions of Logic Programming, International Workshop, T{\"{u}}bingen,
               FRG, December 8-10, 1989, Proceedings},
  pages     = {157--178},
  year      = {1989},
  url       = {https://doi.org/10.1007/BFb0038694},
}

@Article{fleuriot-jcm,
  author =   {Jacques Fleuriot and Lawrence C. Paulson},
  title =   {Mechanizing Nonstandard Real Analysis},
  journal =   {LMS Journal of Computation and Mathematics},
  year =   2000,
  volume =  3,
  pages =  {140-190},
  note =  {\url{http://www.lms.ac.uk/jcm/3/lms1999-027/}}
}

@TechReport{frost93,
  author = {Jacob Frost},
  title  = {A Case Study of Co-induction in {Isabelle HOL}},
  institution = CUCL,
  number = 308,
  year  = 1993,
  month  = Aug}

%revised version of frost93
@TechReport{frost95,
  author = {Jacob Frost},
  title  = {A Case Study of Co-induction in {Isabelle}},
  institution = CUCL,
  number = 359,
  year  = 1995,
  month  = Feb}

@inproceedings{OBJ,
  author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
   and J. Meseguer},
  title  = {Principles of {OBJ2}},
  booktitle = POPL,
  year  = 1985,
  pages  = {52-66}}

%G

@book{gallier86,
  author = {J. H. Gallier},
  title  = {Logic for Computer Science:
  Foundations of Automatic Theorem Proving},
  year  = 1986,
  publisher = {Harper \& Row}}

@Book{galton90,
  author = {Antony Galton},
  title  = {Logic for Information Technology},
  publisher = {Wiley},
  year  = 1990}

@Article{Gentzen:1935,
  author =       {G. Gentzen},
  title =        {Untersuchungen {\"u}ber das logische {S}chlie{\ss}en},
  journal =      {Math. Zeitschrift},
  year =         1935
}

@InProceedings{gimenez-codifying,
  author = {Eduardo Gim{\'e}nez},
  title  = {Codifying Guarded Definitions with Recursive Schemes},
  crossref = {types94},
  pages  = {39-59}
}

@book{girard89,
  author = {Jean-Yves Girard},
  title  = {Proofs and Types},
  year  = 1989,
  publisher = CUP,
  note  = {Translated by Yves Lafont and Paul Taylor}}

@TechReport{Gordon:1985:HOL,
  author =       {M. J. C. Gordon},
  title =        {{HOL}: A machine oriented formulation of higher order logic},
  institution =  {University of Cambridge Computer Laboratory},
  year =         1985,
  number =       68
}

@Book{mgordon-hol,
  editor = {M. J. C. Gordon and T. F. Melham},
  title  = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
  publisher = CUP,
  year  = 1993}

@book{mgordon79,
  author = {Michael J. C. Gordon and Robin Milner and Christopher P.
   Wadsworth},
  title  = {Edinburgh {LCF}: A Mechanised Logic of Computation},
  year  = 1979,
  publisher = {Springer},
  series = LNCS,
  volume = 78}

@inproceedings{Gunter-HOL92,author={Elsa L. Gunter},
title={Why we can't have {SML} style datatype declarations in {HOL}},
booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.java.lang.NullPointerException
IFIP TC10/WG10.2 Intl. Workshop, 1992},
editor={L.J.M. Claesen and M.J.C. Gordon},
publisher=NH,year=1993,pages={561--568}}

@InProceedings{gunter-trees,
  author = {Elsa L. Gunter},
  title  = {A Broader Class of Trees for Recursive Type Definitions for
    {HOL}},
  crossref = {hug93},
  pages  = {141-154}}

%H

@manual{Haftmann-codegen,author={Florian Haftmann},
title={Code generation from {Isabelle/HOL} theories},
note={\url{http://isabelle.in.tum.de/doc/codegen.pdf}}}

@inproceedings{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement,
  author =      {Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow},
  title =       {Data Refinement in {Isabelle/HOL}},
  booktitle =   {Interactive Theorem Proving (ITP 2013)},
  pages =       {100-115},
  year =        2013,
  publisher =   Springer,
  series =      {Lecture Notes in Computer Science},
  volume =      {7998},
  editor =      {S. Blazy and C. Paulin-Mohring and D. Pichardie}
}

@inproceedings{Haftmann-Nipkow:2010:code,
  author =      {Florian Haftmann and Tobias Nipkow},
  title =       {Code Generation via Higher-Order Rewrite Systems},
  booktitle =   {Functional and Logic Programming: 10th International Symposium: FLOPS 2010},
  year =        2010,
  publisher =   Springer,
  series =      LNCS,
  editor =      {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
  volume =      6009
}

@InProceedings{Haftmann-Wenzel:2006:classes,
  author        = {Florian Haftmann and Makarius Wenzel},
  title         = {Constructive Type Classes in {Isabelle}},
  editor        = {T. Altenkirch and C. McBride},
  booktitle     = {Types for Proofs and Programs, TYPES 2006},
  publisher     = {Springer},
  series        = {LNCS},
  volume        = {4502},
  year          = {2007}
}

@InProceedings{Haftmann-Wenzel:2009,
  author        = {Florian Haftmann and Makarius Wenzel},
  title         = {Local theory specifications in {Isabelle/Isar}},
  editor        = {Stefano Berardi and Ferruccio Damiani and de Liguoro, Ugo},
  booktitle     = {Types for Proofs and Programs, TYPES 2008},
  publisher     = {Springer},
  series        = {LNCS},
  volume        = {5497},
  year          = {2009}
}

@inproceedings{hindleymilner,
  author = {L. Damas and H. Milner},
  title = {Principal type schemes for functional programs},
  booktitle = {ACM Symp. Principles of Programming Languages},
  year = 1982
}

@manual{isabelle-classes,
  author        = {Florian Haftmann},
  title         = {Haskell-style type classes with {Isabelle}/{Isar}},
  institution   = TUM,
  note          = {\url{https://isabelle.in.tum.de/doc/classes.pdf}}
}

@manual{isabelle-codegen,
  author        = {Florian Haftmann},
  title         = {Code generation from Isabelle theories},
  institution   = TUM,
  note          = {\url{https://isabelle.in.tum.de/doc/codegen.pdf}}
}

@Book{halmos60,
  author = {Paul R. Halmos},
  title  = {Naive Set Theory},
  publisher = {Van Nostrand},
  year  = 1960}

@book{HarelKT-DL,author={David Harel and Dexter Kozen and Jerzy Tiuryn},
title={Dynamic Logic},publisher=MIT,year=2000}

@Book{hennessy90,
  author = {Matthew Hennessy},
  title  = {The Semantics of Programming Languages: An Elementary
    Introduction Using Structural Operational Semantics},
  publisher = {Wiley},
  year  = 1990}

@article{waldmeister,
  author = {Thomas Hillenbrand and Arnim Buch and Rolan Vogt and Bernd L\"ochner},
  title = "Waldmeister: High-Performance Equational Deduction",
  journal = JAR,
  volume = 18,
  number = 2,
  pages  = {265--270},
  year  = 1997}

@article{hinze10,
  author  = {Hinze, Ralf},
  title   = {Concrete stream calculus---{A}n extended study},
  journal = {J. Funct. Program.},
  volume  = {20},
  issue   = {Special Issue 5-6},
  year    = {2010},
  issn    = {1469-7653},
  pages   = {463--535}
}

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

@book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman},
title={Introduction to Automata Theory, Languages, and Computation.},
publisher={Addison-Wesley},year=1979}

@Article{haskell-report,
  author = {Paul Hudak and Simon Peyton Jones and Philip Wadler},
  title  = {Report on the Programming Language {Haskell}: A
   Non-strict, Purely Functional Language},
  journal = SIGPLAN,
  year  = 1992,
  volume = 27,
  number = 5,
  month  = May,
  note  = {Version 1.2}}

@Article{haskell-tutorial,
  author = {Paul Hudak and Joseph H. Fasel},
  title  = {A Gentle Introduction to {Haskell}},
  journal = SIGPLAN,
  year  = 1992,
  volume = 27,
  number = 5,
  month  = May}

@inproceedings{Hoelzl-Huffman-Immler:2013:typeclasses,
  author    = {Johannes H{\"o}lzl and Fabian Immler and Brian Huffman},
  title     = {Type Classes and Filters for Mathematical Analysis in {Isabelle/HOL}},
  booktitle = {Interactive Theorem Proving (ITP 2013)},
  editor    = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
  year      = 2013,
  volume    = 7998,
  series    = LNCS,
  publisher = Springer,
  isbn      = {978-3-642-39633-5},
  pages     = {279--294}}

@book{Hudak-Haskell,author={Paul Hudak},
title={The Haskell School of Expression},publisher=CUP,year=2000}

@article{huet75,
  author = {G. P. Huet},
  title  = {A Unification Algorithm for Typed $\lambda$-Calculus},
  journal = TCS,
  volume = 1,
  year  = 1975,
  pages  = {27-57}}

@article{huet78,
  author = {G. P. Huet and B. Lang},
  title  = {Proving and Applying Program Transformations Expressed with
   Second-Order Patterns},
  journal = acta,
  volume = 11,
  year  = 1978,
  pages  = {31-55}}

@inproceedings{huet88,
  author = {G{\'e}rard Huet},
  title  = {Induction Principles Formalized in the {Calculus of
   Constructions}},
  booktitle = {Programming of Future Generation Computers},
  editor = {K. Fuchi and M. Nivat},
  year  = 1988,
  pages  = {205-216},
  publisher = {Elsevier}}

@inproceedings{Huffman-Kuncar:2013:lifting_transfer,
  author =      {Brian Huffman and Ond\v{r}ej Kun\v{c}ar},
  title =       {{Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL}},
  booktitle =   {Certified Programs and Proofs (CPP 2013)},
  year =        2013,
  publisher =   Springer,
  series =      {Lecture Notes in Computer Science},
  volume =      {8307},
}

@Book{Huth-Ryan-book,
  author = {Michael Huth and Mark Ryan},
  title  = {Logic in Computer Science. Modelling and reasoning about systems},
  publisher = CUP,
  year  = 2000}

@InProceedings{Harrison:1996:MizarHOL,
  author =   {J. Harrison},
  title =   {A {Mizar} Mode for {HOL}},
  pages =  {203--220},
  crossref =     {tphols96}}

@misc{metis,
  author = "Joe Hurd",
  title = "Metis Theorem Prover",
  note = "\url{http://www.gilith.com/software/metis/}"}

%J

@article{haskell-revised-report,
  author =  {Simon {Peyton Jones} and others},
  title =   {The {Haskell} 98 Language and Libraries: The Revised Report},
  journal = {Journal of Functional Programming},
  volume =  13,
  number =  1,
  pages =   {0--255},
  month =   {Jan},
  year =    2003,
  note =    {\url{http://www.haskell.org/definition/}}}

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

%K

@InProceedings{kammueller-locales,
  author =   {Florian Kamm{\"u}ller and Markus Wenzel and
                  Lawrence C. Paulson},
  title =   {Locales: A Sectioning Concept for {Isabelle}},
  crossref =  {tphols99}}

@book{Knuth3-75,
  author={Donald E. Knuth},
  title={The Art of Computer Programming, Volume 3: Sorting and Searching},
  publisher={Addison-Wesley},
  year=1975}

@Article{korf85,
  author = {R. E. Korf},
  title  = {Depth-First Iterative-Deepening: an Optimal Admissible
   Tree Search},
  journal = AI,
  year  = 1985,
  volume = 27,
  pages  = {97-109}}

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

@inproceedings{korovin-sticksel-2010,
  author    = {Konstantin Korovin and
               Christoph Sticksel},
  title     = {{iP}rover-{E}q: An Instantiation-Based Theorem Prover with Equality},
  pages     = {196--202},
  booktitle={Automated Reasoning: IJCAR 2010},
  editor={J. Giesl and R. H\"ahnle},
  publisher = Springer,
  series = LNCS,
  volume = 6173,
  year = 2010}

@InProceedings{krauss2006,
  author   =  {Alexander Krauss},
  title    =  {Partial Recursive Functions in {Higher-Order Logic}},
  crossref =  {ijcar2006},
  pages =     {589--603}}

@PhdThesis{krauss_phd,
author = {Alexander Krauss},
title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
  school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
year = {2009},
address = {Germany}
}

@manual{isabelle-function,
  author        = {Alexander Krauss},
  title         = {Defining Recursive Functions in {Isabelle/HOL}},
  institution   = TUM,
  note          = {\url{https://isabelle.in.tum.de/doc/functions.pdf}}
}

@inproceedings{Kuncar:2015,
  author    = {Ondrej Kuncar},
  title     = {Correctness of {Isabelle's} Cyclicity Checker: Implementability of Overloading
               in Proof Assistants},
  booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
               {CPP} 2015, Mumbai, India, January 15-17, 2015},
  year      = {2015},
  url       = {http://doi.acm.org/10.1145/2676724.2693175},
  doi       = {10.1145/2676724.2693175},
}

@inproceedings{Kuncar-Popescu:2015,
  author    = {Ondrej Kuncar and Andrei Popescu},
  title     = {A Consistent Foundation for {Isabelle/HOL}},
  editor    = {Christian Urban and Xingyuan Zhang},
  booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP}
               2015, Nanjing, China, August 24-27, 2015, Proceedings},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-319-22102-1_16},
  series    = {Lecture Notes in Computer Science},
  volume    = {9236},
  publisher = {Springer},
}

@Book{kunen80,
  author = {Kenneth Kunen},
  title  = {Set Theory: An Introduction to Independence Proofs},
  publisher = NH,
  year  = 1980}

%L

@manual{OCaml,
  author =  {Xavier Leroy and others},
  title =   {The Objective Caml system -- Documentation and user's manual},
  note =    {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}}

@inproceedings{agsyHOL,
  author    = {Fredrik Lindblad},
  editor    = {St{\'{e}}phane Demri and
               Deepak Kapur and
               Christoph Weidenbach},
  title     = {A Focused Sequent Calculus for Higher-Order Logic},
  booktitle = {Automated Reasoning --- IJCAR 2014},
  series    = {Lecture Notes in Computer Science},
  volume    = {8562},
  pages     = {61--75},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-08587-6\_5},
  doi       = {10.1007/978-3-319-08587-6\_5},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/conf/cade/Lindblad14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}}

@incollection{lochbihler-2010,
  title = "Coinductive",
  author = "Andreas Lochbihler",
  booktitle = "The Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
  publisher = "\url{https://isa-afp.org/entries/Coinductive.shtml}",
  month = "Feb.",
  year = 2010}

@inproceedings{lochbihler-hoelzl-2014,
  author    = {Andreas Lochbihler and
               Johannes H{\"{o}}lzl},
  title     = {Recursive Functions on Lazy Lists via Domains and Topologies},
  booktitle = {Interactive Theorem Proving --- 5th International Conference, {ITP}
               2014},
  pages     = {341--357},
  year      = {2014},
  editor    = {Gerwin Klein and
               Ruben Gamboa},
  series    = LNCS,
  volume    = {8558},
  publisher = {Springer},
}

@book{loveland-78,
  author = "D. W. Loveland",
  title = "Automated Theorem Proving: A Logical Basis",
  year = 1978,
  publisher = "North-Holland Publishing Co."}

@InProceedings{lowe-fdr,
  author = {Gavin Lowe},
  title  = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
    Protocol using {CSP} and {FDR}},
  booktitle =   {Tools and Algorithms for the Construction and Analysis
                  of Systems:  second international workshop, TACAS '96},
  editor =  {T. Margaria and B. Steffen},
  series =  {LNCS 1055},
  year =  1996,
  publisher =  {Springer},
  pages  = {147-166}}

%M

@Article{mw81,
  author = {Zohar Manna and Richard Waldinger},
  title  = {Deductive Synthesis of the Unification Algorithm},
  journal = SCP,
  year  = 1981,
  volume = 1,
  number = 1,
  pages  = {5-48}}

@InProceedings{martin-nipkow,
  author = {Ursula Martin and Tobias Nipkow},
  title  = {Ordered Rewriting and Confluence},
  crossref = {cade10},
  pages  = {366-380}}

@book{martinlof84,
  author = {Per Martin-L{\"o}f},
  title  = {Intuitionistic type theory},
  year  = 1984,
  publisher = {Bibliopolis}}

@inproceedings{Matichuk-et-al:2014,
  author    = {Daniel Matichuk and Makarius Wenzel and Toby C. Murray},
  title     = {An {Isabelle} Proof Method Language},
  editor    = {Gerwin Klein and Ruben Gamboa},
  booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-08970-6_25},
  doi       = {10.1007/978-3-319-08970-6_25},
  series    = "LNCS",
  volume    = {8558},
  publisher = {Springer},
}

@incollection{melham89,
  author = {Thomas F. Melham},
  title  = {Automating Recursive Type Definitions in Higher Order
   Logic},
  pages  = {341-386},
  crossref = {birtwistle89}}

@Article{Miller:1991,
  author =   {Dale Miller},
  title =   {A Logic Programming Language with Lambda-Abstraction, Function Variables,
    and Simple Unification},
  journal =   {Journal of Logic and Computation},
  year =   1991,
  volume =  1,
  number =  4
}

@Article{miller-mixed,
  Author = {Dale Miller},
  Title  = {Unification Under a Mixed Prefix},
  journal = JSC,
  volume = 14,
  number = 4,
  pages  = {321-358},
  Year  = 1992}

@Article{milner78,
  author = {Robin Milner},
  title  = {A Theory of Type Polymorphism in Programming},
  journal = "J. Comp.\ Sys.\ Sci.",
  year  = 1978,
  volume = 17,
  pages  = {348-375}}

@TechReport{milner-ind,
  author = {Robin Milner},
  title  = {How to Derive Inductions in {LCF}},
  institution = Edinburgh,
  year  = 1980,
  type  = {note}}

@Article{milner-coind,
  author = {Robin Milner and Mads Tofte},
  title  = {Co-induction in Relational Semantics},
  journal = TCS,
  year  = 1991,
  volume = 87,
  pages  = {209-220}}

@Book{milner89,
  author = {Robin Milner},
  title  = {Communication and Concurrency},
  publisher = Prentice,
  year  = 1989}

@book{SML,author="Robin Milner and Mads Tofte and Robert Harper",
title="The Definition of Standard ML",publisher=MIT,year=1990}

@PhdThesis{monahan84,
  author = {Brian Q. Monahan},
  title  = {Data Type Proofs using Edinburgh {LCF}},
  school = {University of Edinburgh},
  year  = 1984}

@article{MuellerNvOS99,
author=
{Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
title={{HOLCF = HOL + LCF}},journal=JFP,year=1999,volume=9,pages={191--223}}

@Manual{Muzalewski:Mizar,
  title =   {An Outline of {PC} {Mizar}},
  author =  {Micha{\l} Muzalewski},
  organization = {Fondation of Logic, Mathematics and Informatics
                  --- Mizar Users Group},
  year =  1993,
  note =  {\url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}}
}

%N

@InProceedings{NaraschewskiW-TPHOLs98,
  author = {Wolfgang Naraschewski and Markus Wenzel},
  title  =
{Object-Oriented Verification based on Record Subtyping in
                  Higher-Order Logic},
  crossref      = {tphols98}}

@inproceedings{nazareth-nipkow,
  author = {Dieter Nazareth and Tobias Nipkow},
  title  = {Formal Verification of Algorithm {W}: The Monomorphic Case},
  crossref = {tphols96},
  pages  = {331-345},
  year  = 1996}

@Article{needham-schroeder,
  author =       "Roger M. Needham and Michael D. Schroeder",
  title =        "Using Encryption for Authentication in Large Networks
                 of Computers",
  journal =      cacm,
  volume =       21,
  number =       12,
  pages =        "993-999",
  month =        dec,
  year =         1978}

@inproceedings{nipkow-W,
  author = {Wolfgang Naraschewski and Tobias Nipkow},
  title  = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
  booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96},
  editor = {E. Gim{\'e}nez and C. Paulin-Mohring},
  publisher = Springer,
  series = LNCS,
  volume = 1512,
  pages  = {317-332},
  year  = 1998}

@InCollection{nipkow-sorts93,
  author =   {T. Nipkow},
  title =   {Order-Sorted Polymorphism in {Isabelle}},
  booktitle =   {Logical Environments},
  publisher =  CUP,
  year =  1993,
  editor =  {G. Huet and G. Plotkin},
  pages =  {164--188}
}

@Misc{nipkow-types93,
  author =  {Tobias Nipkow},
  title =  {Axiomatic Type Classes (in {I}sabelle)},
  howpublished = {Presentation at the workshop \emph{Types for Proof and Programs}, Nijmegen},
  year =  1993
}

@inproceedings{Nipkow-CR,
  author = {Tobias Nipkow},
  title  = {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
  booktitle = {Automated Deduction --- CADE-13},
  editor = {M. McRobbie and J.K. Slaney},
  publisher = Springer,
  series = LNCS,
  volume = 1104,
  pages  = {733-747},
  year  = 1996}

% WAS Nipkow-LICS-93
@InProceedings{nipkow-patterns,
  title  = {Functional Unification of Higher-Order Patterns},
  author = {Tobias Nipkow},
  pages  = {64-74},
  crossref = {lics8},
  url  = {\url{ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html}},
  keywords = {unification}}

@article{nipkow-IMP,
  author = {Tobias Nipkow},
  title  = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
  journal = FAC,
  volume = 10,
  pages  = {171-186},
  year  = 1998}

@inproceedings{Nipkow-TYPES02,
  author        = {Tobias Nipkow},
  title         = {{Structured Proofs in Isar/HOL}},
  booktitle     = {Types for Proofs and Programs (TYPES 2002)},
  editor        = {H. Geuvers and F. Wiedijk},
  year          = 2003,
  publisher     = Springer,
  series        = LNCS,
  volume        = 2646,
  pages         = {259-278}}

@manual{isabelle-HOL,
  author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title  = {{Isabelle}'s Logics: {HOL}},
  institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t
                  M{\"u}nchen and Computer Laboratory, University of Cambridge},
  note          = {\url{https://isabelle.in.tum.de/doc/logics-HOL.pdf}}}

@article{nipkow-prehofer,
  author = {Tobias Nipkow and Christian Prehofer},
  title  = {Type Reconstruction for Type Classes},
  journal = JFP,
  volume = 5,
  number = 2,
  year  = 1995,
  pages  = {201-224}}

@InProceedings{Nipkow-Prehofer:1993,
  author =       {T. Nipkow and C. Prehofer},
  title =        {Type checking type classes},
  booktitle =    {ACM Symp.\ Principles of Programming Languages},
  year =         1993
}

@Book{isa-tutorial,
  author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title  = {Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic},
  publisher = Springer,
  year  = 2002,
  series    = LNCS,
  volume    = 2283}

@Article{noel,
  author = {Philippe No{\"e}l},
  title  = {Experimenting with {Isabelle} in {ZF} Set Theory},
  journal = JAR,
  volume = 10,
  number = 1,
  pages  = {15-58},
  year  = 1993}

@book{nordstrom90,
  author = {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith},
  title  = {Programming in {Martin-L{\"o}f}'s Type Theory. An
   Introduction},
  publisher = {Oxford University Press},
  year  = 1990}

%O

@TechReport{scala-overview-tech-report,
  author =       {Martin Odersky et al.},
  title =        {An Overview of the Scala Programming Language},
  institution =  {EPFL Lausanne, Switzerland},
  year =         2004,
  number =       {IC/2004/64}
}

@Article{Oppen:1980,
  author =       {D. C. Oppen},
  title =        {Pretty Printing},
  journal =      {ACM Transactions on Programming Languages and Systems},
  year =         1980,
  volume =    2,
  number =    4}

@Manual{pvs-language,
  title  = {The {PVS} specification language},
  author = {S. Owre and N. Shankar and J. M. Rushby},
  organization = {Computer Science Laboratory, SRI International},
  address = {Menlo Park, CA},
  note          = {Beta release},
  year  = 1993,
  month  = apr,
  url  = {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}}

%P

@inproceedings{panny-et-al-2014,
  author = "Lorenz Panny and Jasmin Christian Blanchette and Dmitriy Traytel",
  title = "Primitively (co)recursive definitions for {I}sabelle/{HOL}",
  year = 2014,
  booktitle = "Isabelle Workshop 2014"
}

% replaces paulin92
@InProceedings{paulin-tlca,
  author = {Christine Paulin-Mohring},
  title  = {Inductive Definitions in the System {Coq}: Rules and
   Properties},
  crossref = {tlca93},
  pages  = {328-345}}

@Article{paulson:1983,
  author =       {L. C. Paulson},
  title =        {A higher-order implementation of rewriting},
  journal =      {Science of Computer Programming},
  year =         1983,
  volume =    3,
  pages =     {119--149},
  note =      {\url{http://www.cl.cam.ac.uk/~lp15/papers/Reports/TR035-lcp-rewriting.pdf}}}

@InProceedings{paulson-CADE,
  author = {Lawrence C. Paulson},
  title  = {A Fixedpoint Approach to Implementing (Co)Inductive
    Definitions},
  pages  = {148-161},
  crossref = {cade12}}

@InProceedings{paulson-COLOG,
  author = {Lawrence C. Paulson},
  title  = {A Formulation of the Simple Theory of Types (for
   {Isabelle})},
  pages  = {246-274},
  crossref = {colog88},
  url  = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}}

@Article{paulson-coind,
  author = {Lawrence C. Paulson},
  title  = {Mechanizing Coinduction and Corecursion in Higher-Order
    Logic},
  journal = JLC,
  year  = 1997,
  volume = 7,
  number = 2,
  month  = mar,
  pages  = {175-204}}

@article{paulson-numerical,
  author        = {Lawrence C. Paulson},
  title         = {Organizing numerical theories using axiomatic type
                  classes},
  journal       = JAR,
  year          = 2004,
  volume        = 33,
  number        = 1,
  pages         = {29-49}}

@manual{isabelle-intro,
  author = {Lawrence C. Paulson},
  title  = {Old Introduction to {Isabelle}},
  institution = CUCL,
  note          = {\url{https://isabelle.in.tum.de/doc/intro.pdf}}}

@manual{isabelle-logics,
  author = {Lawrence C. Paulson},
  title  = {{Isabelle's} Logics},
  institution = CUCL,
  note          = {\url{https://isabelle.in.tum.de/doc/logics.pdf}}}

@manual{isabelle-ref,
  author = {Lawrence C. Paulson},
  title  = {The Old {Isabelle} Reference Manual},
  institution = CUCL,
  note          = {\url{https://isabelle.in.tum.de/doc/ref.pdf}}}

@manual{isabelle-ZF,
  author = {Lawrence C. Paulson},
  title  = {{Isabelle}'s Logics: {FOL} and {ZF}},
  institution = CUCL,
  note          = {\url{https://isabelle.in.tum.de/doc/logics-ZF.pdf}}}

@article{paulson-found,
  author = {Lawrence C. Paulson},
  title  = {The Foundation of a Generic Theorem Prover},
  journal = JAR,
  volume = 5,
  number = 3,
  pages  = {363-397},
  year  = 1989,
  url  = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}}

%replaces paulson-final
@Article{paulson-mscs,
  author = {Lawrence C. Paulson},
  title =   {Final Coalgebras as Greatest Fixed Points
                  in {ZF} Set Theory},
  journal = {Mathematical Structures in Computer Science},
  year  = 1999,
  volume = 9,
  number = 5,
  pages = {545-567}}

@InCollection{paulson-generic,
  author = {Lawrence C. Paulson},
  title  = {Generic Automatic Proof Tools},
  crossref = {wos-fest},
  chapter = 3}

@Article{paulson-gr,
  author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
  title  = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of
    Choice},
  journal = JAR,
  year  = 1996,
  volume = 17,
  number = 3,
  month  = dec,
  pages  = {291-323}}

@InCollection{paulson-fixedpt-milner,
  author = {Lawrence C. Paulson},
  title  = {A Fixedpoint Approach to (Co)inductive and
                  (Co)datatype Definitions},
  pages  = {187-211},
  crossref = {milner-fest}}

@book{milner-fest,
  title  = {Proof, Language, and Interaction:
                   Essays in Honor of {Robin Milner}},
  booktitle = {Proof, Language, and Interaction:
                   Essays in Honor of {Robin Milner}},
  publisher = MIT,
  year  = 2000,
  editor = {Gordon Plotkin and Colin Stirling and Mads Tofte}}

@InCollection{paulson-handbook,
  author = {Lawrence C. Paulson},
  title  = {Designing a Theorem Prover},
  crossref = {handbk-lics2},
  pages  = {415-475}}

@Book{paulson-isa-book,
  author = {Lawrence C. Paulson},
  title  = {Isabelle: A Generic Theorem Prover},
  publisher = {Springer},
  year  = 1994,
  note  = {LNCS 828}}

@Book{isabelle-hol-book,
  author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title  = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher = {Springer},
  year  = 2002,
  note  = {LNCS 2283}}

@InCollection{paulson-markt,
  author = {Lawrence C. Paulson},
  title  = {Tool Support for Logics of Programs},
  booktitle = {Mathematical Methods in Program Development:
                  Summer School Marktoberdorf 1996},
  publisher = {Springer},
  pages  = {461-498},
  year  = {Published 1997},
  editor = {Manfred Broy},
  series = {NATO ASI Series F}}

%replaces Paulson-ML and paulson91
@book{paulson-ml2,
  author = {Lawrence C. Paulson},
  title  = {{ML} for the Working Programmer},
  year  = 1996,
  edition = {2nd},
  publisher = CUP,
  note = {\url{https://www.cl.cam.ac.uk/~lp15/MLbook}}}

@article{paulson-natural,
  author = {Lawrence C. Paulson},
  title  = {Natural Deduction as Higher-order Resolution},
  journal = JLP,
  volume = 3,
  pages  = {237-258},
  year  = 1986,
  url  = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}}

@Article{paulson-set-I,
  author = {Lawrence C. Paulson},
  title  = {Set Theory for Verification: {I}.  {From}
   Foundations to Functions},
  journal = JAR,
  volume = 11,
  number = 3,
  pages  = {353-389},
  year  = 1993,
  url  = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Sets/set-I.pdf}}}

@Article{paulson-set-II,
  author = {Lawrence C. Paulson},
  title  = {Set Theory for Verification: {II}.  {Induction} and
   Recursion},
  journal = JAR,
  volume = 15,
  number = 2,
  pages  = {167-215},
  year  = 1995,
  url  = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}}

@article{paulson85,
  author = {Lawrence C. Paulson},
  title  = {Verifying the Unification Algorithm in {LCF}},
  journal = SCP,
  volume = 5,
  pages  = {143-170},
  year  = 1985}

%replaces Paulson-LCF
@book{paulson87,
  author = {Lawrence C. Paulson},
  title  = {Logic and Computation: Interactive proof with Cambridge
   LCF},
  year  = 1987,
  publisher = CUP}

@incollection{paulson700,
  author = {Lawrence C. Paulson},
  title  = {{Isabelle}: The Next 700 Theorem Provers},
  crossref = {odifreddi90},
  pages  = {361-386},
  url  = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}}

% replaces paulson-ns and paulson-security
@Article{paulson-jcs,
  author = {Lawrence C. Paulson},
  title  = {The Inductive Approach to Verifying Cryptographic Protocols},
  journal = JCS,
  year  = 1998,
  volume = 6,
  pages  = {85-128}}

@Article{paulson-tls,
  author =   {Lawrence C. Paulson},
  title =   {Inductive Analysis of the {Internet} Protocol {TLS}},
  journal =   TISSEC,
  month =        aug,
  year =   1999,
  volume = 2,
  number        = 3,
  pages  = {332-351}}

@Article{paulson-yahalom,
  author =   {Lawrence C. Paulson},
  title =   {Relations Between Secrets:
                  Two Formal Analyses of the {Yahalom} Protocol},
  journal =   JCS,
  volume = 9,
  number = 3,
  pages = {197-216},
  year = 2001}}

@article{pelletier86,
  author = {F. J. Pelletier},
  title  = {Seventy-five Problems for Testing Automatic Theorem
   Provers},
  journal = JAR,
  volume = 2,
  pages  = {191-216},
  year  = 1986,
  note  = {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}}

@InCollection{pitts93,
  author =       {A. Pitts},
  title =        {The {HOL} Logic},
  editor =       {M. J. C. Gordon and T. F. Melham},
  booktitle  =   {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
  pages =        {191--232},
  publisher = CUP,
  year  = 1993}

@Article{pitts94,
  author = {Andrew M. Pitts},
  title  = {A Co-induction Principle for Recursively Defined Domains},
  journal = TCS,
  volume = 124,
  pages  = {195-219},
  year  = 1994}

@Article{plaisted90,
  author = {David A. Plaisted},
  title  = {A Sequent-Style Model Elimination Strategy and a Positive
   Refinement},
  journal = JAR,
  year  = 1990,
  volume = 6,
  number = 4,
  pages  = {389-402}}

%Q

@Article{quaife92,
  author = {Art Quaife},
  title  = {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set
   Theory},
  journal = JAR,
  year  = 1992,
  volume = 8,
  number = 1,
  pages  = {91-147}}

%R

@TechReport{rasmussen95,
  author = {Ole Rasmussen},
  title  = {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting
    Experiment},
  institution = {Computer Laboratory, University of Cambridge},
  year  = 1995,
  number = 364,
  month  = may,
  url  = {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}}

@Book{reeves90,
  author = {Steve Reeves and Michael Clarke},
  title  = {Logic for Computer Science},
  publisher = {Addison-Wesley},
  year  = 1990}

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

@book{Rosen-DMA,author={Kenneth H. Rosen},
title={Discrete Mathematics and Its Applications},
publisher={McGraw-Hill},year=1998}

@InProceedings{Rudnicki:1992:MizarOverview,
  author =   {P. Rudnicki},
  title =   {An Overview of the {MIZAR} Project},
  booktitle =   {1992 Workshop on Types for Proofs and Programs},
  year =  1992,
  organization = {Chalmers University of Technology},
  publisher =  {Bastad}
}

@article{rutten05,
  author    = {Jan J. M. M. Rutten},
  title     = {A coinductive calculus of streams},
  journal   = {Math. Struct. Comp. Sci.},
  volume    = 15,
  number    = 1,
  year      = 2005,
  pages     = {93--147},
}

%S

@inproceedings{saaltink-fme,
  author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
   Dan Craigen and Irwin Meisels},
  title  = {An {EVES} Data Abstraction Example},
  pages  = {578-596},
  crossref = {fme93}}

@Article{Schroeder-Heister:1984,
  author =       {Peter Schroeder-Heister},
  title =        {A Natural Extension of Natural Deduction},
  journal =      {Journal of Symbolic Logic},
  year =         1984,
  volume =       49,
  number =       4
}

@inproceedings{schulz-2019,
  author    = {Stephan Schulz and
               Simon Cruanes and
               Petar Vukmirovi\'c},
  editor    = {Pascal Fontaine},
  title     = {Faster, Higher, Stronger: {E} 2.3},
  booktitle = {Automated Deduction --- {CADE}-27},
  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},
  doi       = {10.1007/978-3-030-29436-6\_29},
  timestamp = {Sat, 19 Oct 2019 20:28:03 +0200},
  biburl    = {https://dblp.org/rec/conf/cade/0001CV19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}}

@inproceedings{slind-tfl,
  author = {Konrad Slind},
  title  = {Function Definition in Higher Order Logic},
  crossref  = {tphols96},
  pages  = {381-397}}

@inproceedings{leo3,
  Author =  {Alexander Steen and Max Wisniewski and Christoph
                  Benzm{\"u}ller},
  Booktitle =  {Mathematical Software -- ICMS 2016},
  Editor =  {G.-M. Greuel and T. Koch and P. Paule and
                  A. Sommese},
  Publisher =  {Springer},
  Series =  {LNCS},
  Title =  {Agent-Based {HOL} Reasoning},
  Volume =  9725,
  Year =  2016,
  Pages =  {75-81}
}

@incollection{sternagel-thiemann-2015,
  title = "Deriving Class Instances for Datatypes",
  author = "Christian Sternagel and Ren\'e Thiemann",
  booktitle = "The Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
  publisher = "\url{https://isa-afp.org/entries/Deriving.shtml}",
  month = "March",
  year = 2015}

@inproceedings{snark,
  author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood},
  title = {Deductive composition of astronomical software from subroutine libraries},
  pages = "341--355",
  crossref = {cade12}}

@book{suppes72,
  author = {Patrick Suppes},
  title  = {Axiomatic Set Theory},
  year  = 1972,
  publisher = {Dover}}

@inproceedings{sutcliffe-2000,
  author = "Geoff Sutcliffe",
  title = "System Description: {SystemOnTPTP}",
  editor = "David McAllester",
  booktitle = {Automated Deduction --- {CADE}-17 International Conference},
  series = "Lecture Notes in Artificial Intelligence",
  volume = {1831},
  pages = "406--410",
  year = 2000,
  publisher = Springer}

@misc{tofof,
  author = "Geoff Sutcliffe",
  title = "{ToFoF}",
  note = "\url{http://www.cs.miami.edu/~tptp/ATPSystems/ToFoF/}"}

@Article{Sutter:2005,
  author =   {H. Sutter},
  title =   {The Free Lunch Is Over --- A Fundamental Turn Toward Concurrency in Software},
  journal =   {Dr. Dobb's Journal},
  year =   2005,
  volume =   30,
  number =   3}

@InCollection{szasz93,
  author = {Nora Szasz},
  title  = {A Machine Checked Proof that {Ackermann's} Function is not
    Primitive Recursive},
  crossref = {huet-plotkin93},
  pages  = {317-338}}

@TechReport{Syme:1997:DECLARE,
  author =   {D. Syme},
  title =   {{DECLARE}: A Prototype Declarative Proof System for Higher Order Logic},
  institution =  {University of Cambridge Computer Laboratory},
  year =   1997,
  number =  416
}

@PhdThesis{Syme:1998:thesis,
  author =   {D. Syme},
  title =   {Declarative Theorem Proving for Operational Semantics},
  school =   {University of Cambridge},
  year =   1998,
  note =  {Submitted}
}

@InProceedings{Syme:1999:TPHOL,
  author =   {D. Syme},
  title =   {Three Tactic Theorem Proving},
  crossref =     {tphols99}}

%T

@book{takeuti87,
  author = {G. Takeuti},
  title  = {Proof Theory},
  year  = 1987,
  publisher = NH,
  edition = {2nd}}

@Book{thompson91,
  author = {Simon Thompson},
  title  = {Type Theory and Functional Programming},
  publisher = {Addison-Wesley},
  year  = 1991}

@book{Thompson-Haskell,author={Simon Thompson},
title={Haskell: The Craft of Functional Programming},
publisher={Addison-Wesley},year=1999}

@misc{kodkod-2009,
  author = "Emina Torlak",
  title = {Kodkod: Constraint Solver for Relational Logic},
  note = "\url{http://alloy.mit.edu/kodkod/}"}

@misc{kodkod-2009-options,
  author = "Emina Torlak",
  title = "Kodkod {API}: Class {Options}",
  note = "\url{http://alloy.mit.edu/kodkod/docs/kodkod/engine/config/Options.html}"}

@inproceedings{torlak-jackson-2007,
  title = "Kodkod: A Relational Model Finder",
  author = "Emina Torlak and Daniel Jackson",
  editor = "Orna Grumberg and Michael Huth",
  booktitle = "TACAS 2007",
  series = LNCS,
  volume = {4424},
  pages = "632--647",
  year = 2007,
  publisher = Springer}

@inproceedings{traytel-berghofer-nipkow-2011,
  author = {Dmitriy Traytel and Stefan Berghofer and Tobias Nipkow},
  title = {{Extending Hindley-Milner Type Inference with Coercive Structural Subtyping}},
  year = 2011,
  editor = {Hongseok Yang},
  booktitle = "APLAS 2011",
  series = LNCS,
  volume = {7078},
  pages = "89--104"}

@inproceedings{traytel-et-al-2012,
  author = "Dmitriy Traytel and Andrei Popescu and Jasmin Christian Blanchette",
  title     = {Foundational, Compositional (Co)datatypes for Higher-Order
               Logic---{C}ategory Theory Applied to Theorem Proving},
  year      = {2012},
  pages     = {596--605},
  booktitle = {27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012},
  publisher = {IEEE}
}

@Unpublished{Trybulec:1993:MizarFeatures,
  author =   {A. Trybulec},
  title =   {Some Features of the {Mizar} Language},
  note =   {Presented at a workshop in Turin, Italy},
  year =  1993
}

%V

@Unpublished{voelker94,
  author = {Norbert V{\"o}lker},
  title  = {The Verification of a Timer Program using {Isabelle/HOL}},
  note  = {\url{ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}},
  year  = 1994,
  month  = aug}

%W

@inproceedings{wadler89how,
  author        = {P. Wadler and S. Blott},
  title         = {How to make ad-hoc polymorphism less ad-hoc},
  booktitle     = {ACM Symp.\ Principles of Programming Languages},
  year          = 1989
}

@phdthesis{weber-2008,
  author = "Tjark Weber",
  title = "SAT-Based Finite Model Generation for Higher-Order Logic",
  school = {Dept.\ of Informatics, T.U. M\"unchen},
  type = "{Ph.D.}\ thesis",
  year = 2008}

@Misc{x-symbol,
  author =  {Christoph Wedler},
  title =  {Emacs package ``{X-Symbol}''},
  note =  {\url{http://x-symbol.sourceforge.net}}
}

@inproceedings{weidenbach-et-al-2009,
  author    = {Christoph Weidenbach and
               Dilyana Dimova and
               Arnaud Fietzke and
               Rohit Kumar and
               Martin Suda and
               Patrick Wischnewski},
  editor    = {Renate A. Schmidt},
  title     = {{SPASS} Version 3.5},
  booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated
               Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5663},
  pages     = {140--145},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-02959-2\_10},
  doi       = {10.1007/978-3-642-02959-2\_10},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/conf/cade/WeidenbachDFKSW09.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@manual{isabelle-system,
  author = {Makarius Wenzel},
  title = {The {Isabelle} System Manual},
  note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}}

@manual{isabelle-jedit,
  author = {Makarius Wenzel},
  title = {{Isabelle/jEdit}},
  note = {\url{https://isabelle.in.tum.de/doc/jedit.pdf}}}

@manual{isabelle-isar-ref,
  author = {Makarius Wenzel},
  title = {The {Isabelle/Isar} Reference Manual},
  note = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}}

@manual{isabelle-implementation,
  author = {Makarius Wenzel},
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.