% 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{satallax,

   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{http://isabelle.in.tum.de/doc/locales.pdf}}

 }

 @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{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}

 }

 @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{http://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},

   editor = 	 {G. Sutcliffe and A. Voronkov},

   volume = 	 3835,

   series = 	 LNCS,

   publisher = Springer}

 @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/{HOL}},

   institution   = TUM,

   note          = {\url{http://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/{HOL}},

   institution   = TUM,

   note          = {\url{http://isabelle.in.tum.de/doc/sledgehammer.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{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}

 @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}

 @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

 @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}

 %D

 @Book{davey-priestley,

   author	= {B. A. Davey and H. A. Priestley},

   title		= {Introduction to Lattices and Order},

   publisher	= CUP,

   year		= 1990}

 @Book{devlin79,

   author	= {Keith J. Devlin},

   title		= {Fundamentals of Contemporary Set Theory},

   publisher	= {Springer},

   year		= 1979}

 @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}}

 @InProceedings{felty91a,

   Author	= {Amy Felty},

   Title		= {A Logic Program for Transforming Sequent Proofs to Natural

 		  Deduction Proofs}, 

   crossref	= {extensions91},

   pages		= {157-178}}

 @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}}

 @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 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.\

 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

 @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-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: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}

 }

 @manual{isabelle-classes,

   author        = {Florian Haftmann},

   title         = {Haskell-style type classes with {Isabelle}/{Isar}},

   institution   = TUM,

   note          = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}

 }

 @manual{isabelle-codegen,

   author        = {Florian Haftmann},

   title         = {Code generation from Isabelle theories},

   institution   = TUM,

   note          = {\url{http://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}

 @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{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,

   editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",

   year = 2011,

   note = "To appear."}

 @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}}

 @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{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{http://isabelle.in.tum.de/doc/functions.pdf}}

 }

 @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/}}}

 @incollection{lochbihler-2010,

   title = "Coinduction",

   author = "Andreas Lochbihler",

   booktitle = "The Archive of Formal Proofs",

   editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",

   publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",

   month = "Feb.",

   year = 2010}

 @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}}

 @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{http://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 and al.},

   title =        {An Overview of the Scala Programming Language},

   institution =  {EPFL Lausanne, Switzerland},

   year =         2004,

   number =       {IC/2004/64}

 }

 @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

 % replaces paulin92

 @InProceedings{paulin-tlca,

   author	= {Christine Paulin-Mohring},

   title		= {Inductive Definitions in the System {Coq}: Rules and

 		 Properties},

   crossref	= {tlca93},

   pages		= {328-345}}

 @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}}

 @manual{isabelle-intro,

   author	= {Lawrence C. Paulson},

   title		= {Old Introduction to {Isabelle}},

   institution	= CUCL,

   note          = {\url{http://isabelle.in.tum.de/doc/intro.pdf}}}

 @manual{isabelle-logics,

   author	= {Lawrence C. Paulson},

   title		= {{Isabelle's} Logics},

   institution	= CUCL,

   note          = {\url{http://isabelle.in.tum.de/doc/logics.pdf}}}

 @manual{isabelle-ref,

   author	= {Lawrence C. Paulson},

   title		= {The Old {Isabelle} Reference Manual},

   institution	= CUCL,

   note          = {\url{http://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{http://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}

 @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}

 }

 %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

 }

 @article{schulz-2002,

   author = "Stephan Schulz",

   title = "E---A Brainiac Theorem Prover",

   journal = "Journal of AI Communications",

   year = 2002,

   volume = 15,

   number ="2/3",

   pages = "111--126"}

 @misc{sledgehammer-2009,

   key = "Sledgehammer",

   title = "The {S}ledgehammer: Let Automatic Theorem Provers

 Write Your {I}s\-a\-belle Scripts",

   note = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/sledgehammer.html}"}

 @inproceedings{slind-tfl,

   author	= {Konrad Slind},

   title		= {Function Definition in Higher Order Logic},

   crossref  = {tphols96},

   pages		= {381-397}}

 @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}

 @unpublished{traytel-berghofer-nipkow-2011,

   author = {D. Traytel and S. Berghofer and T. Nipkow},

   title = {Extending Hindley-Milner Type Inference with Coercive

       Subtyping (long version)},

   year = 2011,

   note = {Submitted,

       \url{http://isabelle.in.tum.de/doc/implementation.pdf}}},

 }

 @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}},

   url		= {\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}}

 }

 @misc{weidenbach-et-al-2009,

   author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski",

   title = "{SPASS} Version 3.5",

   note = {\url{http://www.spass-prover.org/publications/spass.pdf}}}

 @manual{isabelle-sys,

   author	= {Markus Wenzel and Stefan Berghofer},

   title		= {The {Isabelle} System Manual},

   institution	= {TU Munich},

   note          = {\url{http://isabelle.in.tum.de/doc/system.pdf}}}

 @manual{isabelle-isar-ref,

   author	= {Makarius Wenzel},

   title		= {The {Isabelle/Isar} Reference Manual},

   institution	= {TU Munich},

   note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}

 @manual{isabelle-implementation,

   author	= {Makarius Wenzel},

   title		= {The {Isabelle/Isar} Implementation},

   institution	= {TU Munich},

   note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}

 @InProceedings{Wenzel:1999:TPHOL,

   author = 	 {Markus Wenzel},

   title = 	 {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},

   crossref =     {tphols99}}

 @InProceedings{Wenzel:1997:TPHOL,

   author = 	 {Markus Wenzel},

   title = 	 {Type Classes and Overloading in Higher-Order Logic},

   crossref =     {tphols97}}

 @phdthesis{Wenzel-PhD,

   author={Markus Wenzel},

     title={Isabelle/Isar --- a versatile environment for human-readable formal proof documents},

   school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},

   year=2002,

   note =	 {\url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html}}}

 @Article{Wenzel-Wiedijk:2002,

   author = 	 {Freek Wiedijk and Markus Wenzel},

   title = 	 {A comparison of the mathematical proof languages {Mizar} and {Isar}.},

   journal = 	 {Journal of Automated Reasoning},

   year = 	 2002,

   volume =	 29,

   number =	 {3-4}

 }

 @InCollection{Wenzel-Paulson:2006,

   author = 	 {Markus Wenzel and Lawrence C. Paulson},

   title = 	 {{Isabelle/Isar}},

   booktitle = 	 {The Seventeen Provers of the World},

   year =	 2006,

   editor =	 {F. Wiedijk},

   series =	 {LNAI 3600}

 }

 @InCollection{Wenzel:2006:Festschrift,

   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 =	 {University of Bia{\l}ystok},

   year =	 2007,

   editor =	 {R. Matuszewski and A. Zalewska},

   volume =	 {10(23)},

   series =	 {Studies in Logic, Grammar, and Rhetoric},

   note =         {\url{http://www.in.tum.de/~wenzelm/papers/isar-framework.pdf}}

 }

 @InProceedings{Wenzel-Chaieb:2007b,

   author = {Makarius Wenzel and Amine Chaieb},

   title = {{SML} with antiquotations embedded into {Isabelle/Isar}},

   booktitle = {Workshop on Programming Languages for Mechanized Mathematics

     (satellite of CALCULEMUS 2007). Hagenberg, Austria},

   editor = {Jacques Carette and Freek Wiedijk},

   month = {June},

   year = {2007}

 }

 @InProceedings{Wenzel:2009,

   author = 	 {M. Wenzel},

   title = 	 {Parallel Proof Checking in {Isabelle/Isar}},

   booktitle = {ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009)},

   year = 	 2009,

   editor = 	 {Dos Reis, G. and L. Th\'ery},

   publisher = {ACM Digital Library}}

 @book{principia,

   author	= {A. N. Whitehead and B. Russell},

   title		= {Principia Mathematica},

   year		= 1962,

   publisher	= CUP, 

   note		= {Paperback edition to *56,

   abridged from the 2nd edition (1927)}}

 @Misc{Wiedijk:1999:Mizar,

   author =	 {Freek Wiedijk},

   title =	 {Mizar: An Impression},

   howpublished = {Unpublished paper},

   year =         1999,

   note =	 {\url{http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz}}

 }

 @Misc{Wiedijk:2000:MV,

   author =	 {Freek Wiedijk},

   title =	 {The Mathematical Vernacular},

   howpublished = {Unpublished paper},

   year =         2000,

   note =	 {\url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}}

 }

 @misc{wikipedia-2009-aa-trees,

   key = "Wikipedia",

   title = "Wikipedia: {AA} Tree",

   note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}

 @book{winskel93,

   author	= {Glynn Winskel},

   title		= {The Formal Semantics of Programming Languages},

   publisher	= MIT,year=1993}

 @InCollection{wos-bledsoe,

   author	= {Larry Wos},

   title		= {Automated Reasoning and {Bledsoe's} Dream for the Field},

   crossref	= {bledsoe-fest},

   pages		= {297-342}}

 @InProceedings{Zammit:1999:TPHOL,

   author = 	 {Vincent Zammit},

   title = 	 {On the Implementation of an Extensible Declarative Proof Language},

   crossref =     {tphols99}}

 %Z

 @misc{z3,

   key = "Z3",

   title = "Z3: An Efficient {SMT} Solver",

   note = "\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}"}

 % CROSS REFERENCES

 @book{handbk-lics2,

   editor	= {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},

   title		= {Handbook of Logic in Computer Science},

   booktitle	= {Handbook of Logic in Computer Science},

   publisher	= {Oxford University Press},

   year		= 1992,

   volume	= 2}

 @book{types93,

   editor	= {Henk Barendregt and Tobias Nipkow},

   title		= TYPES # {: International Workshop {TYPES '93}},

   booktitle	= TYPES # {: International Workshop {TYPES '93}},

   year		= {published 1994},

   publisher	= {Springer},

   series	= {LNCS 806}}

 @book{barwise-handbk,

   editor	= {J. Barwise},

   title		= {Handbook of Mathematical Logic},

   booktitle	= {Handbook of Mathematical Logic},

   year		= 1977,

   publisher	= NH}

 @Proceedings{tlca93,

   title		= {Typed Lambda Calculi and Applications},

   booktitle	= {Typed Lambda Calculi and Applications},

   editor	= {M. Bezem and J.F. Groote},

   year		= 1993,

   publisher	= {Springer},

   series	= {LNCS 664}}

 @book{birtwistle89,

   editor	= {Graham Birtwistle and P. A. Subrahmanyam},

   title		= {Current Trends in Hardware Verification and Automated

 		 Theorem Proving}, 

   booktitle	= {Current Trends in Hardware Verification and Automated

 		 Theorem Proving}, 

   publisher	= {Springer},

   year		= 1989}

 @book{bledsoe-fest,

   title		= {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},

   booktitle	= {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},

   publisher	= {Kluwer Academic Publishers},

   year		= 1991,

   editor	= {Robert S. Boyer}}

 @Proceedings{cade12,

   editor	= {Alan Bundy},

   title		= {Automated Deduction --- {CADE}-12 

 		  International Conference},

   booktitle	= {Automated Deduction --- {CADE}-12 

 		  International Conference},

   year		= 1994,

   series	= {LNAI 814},

   publisher	= {Springer}}

 @book{types94,

   editor	= {Peter Dybjer and Bengt Nordstr{{\"o}m} and Jan Smith},

   title		= TYPES # {: International Workshop {TYPES '94}},

   booktitle	= TYPES # {: International Workshop {TYPES '94}},

   year		= 1995,

   publisher	= {Springer},

   series	= {LNCS 996}}

 @book{huet-plotkin91,

   editor	= {{G{\'e}rard} Huet and Gordon Plotkin},

   title		= {Logical Frameworks},

   booktitle	= {Logical Frameworks},

   publisher	= CUP,

   year		= 1991}

 @book{huet-plotkin93,

   editor	= {{G{\'e}rard} Huet and Gordon Plotkin},

   title		= {Logical Environments},

   booktitle	= {Logical Environments},

   publisher	= CUP,

   year		= 1993}

 @Proceedings{hug93,

   editor	= {J. Joyce and C. Seger},

   title		= {Higher Order Logic Theorem Proving and Its

 		  Applications: HUG '93},

   booktitle	= {Higher Order Logic Theorem Proving and Its

 		  Applications: HUG '93},

   year		= {Published 1994},

   publisher	= {Springer},

   series	= {LNCS 780}}

 @proceedings{colog88,

   editor	= {P. Martin-L{\"o}f and G. Mints},

   title		= {COLOG-88: International Conference on Computer Logic},

   booktitle	= {COLOG-88: International Conference on Computer Logic},

   year		= {Published 1990},

   publisher	= {Springer},

   organization	= {Estonian Academy of Sciences},

   address	= {Tallinn},

   series	= {LNCS 417}}

 @book{odifreddi90,

   editor	= {P. Odifreddi},

   title		= {Logic and Computer Science},

   booktitle	= {Logic and Computer Science},

   publisher	= {Academic Press},

   year		= 1990}

 @proceedings{extensions91,

   editor	= {Peter Schroeder-Heister},

   title		= {Extensions of Logic Programming},

   booktitle	= {Extensions of Logic Programming},

   year		= 1991,

   series	= {LNAI 475}, 

   publisher	= {Springer}}

 @proceedings{cade10,

   editor	= {Mark E. Stickel},

   title		= {10th } # CADE,

   booktitle	= {10th } # CADE,

   year		= 1990,

   publisher	= {Springer},

   series	= {LNAI 449}}

 @Proceedings{lics8,

   editor	= {M. Vardi},

   title		= {Eighth Annual Symposium on Logic in Computer Science},

   booktitle	= {Eighth Annual Symposium on Logic in Computer Science},

   publisher	= IEEE,

   year		= 1993}

 @book{wos-fest,

   title		= {Automated Reasoning and its Applications: 

 			Essays in Honor of {Larry Wos}},

   booktitle	= {Automated Reasoning and its Applications: 

 			Essays in Honor of {Larry Wos}},

   publisher	= MIT,

   year		= 1997,

   editor	= {Robert Veroff}}

 @proceedings{fme93,

   editor	= {J. C. P. Woodcock and P. G. Larsen},

   title		= {FME '93: Industrial-Strength Formal Methods},

   booktitle	= {FME '93: Industrial-Strength Formal Methods},

   year		= 1993,

   publisher	= Springer,

   series	= LNCS,

   volume        = 670}

 @Proceedings{tphols96,

   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '96},

   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '96},

   editor	= {J. von Wright and J. Grundy and J. Harrison},

   publisher     = Springer,

   series	= LNCS,

   volume        = 1125,

   year		= 1996}

 @Proceedings{tphols97,

   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '97},

   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '97},

   editor	= {Elsa L. Gunter and Amy Felty},

   publisher     = Springer,

   series	= LNCS,

   volume        = 1275,

   year		= 1997}

 @Proceedings{tphols98,

   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},

   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},

   editor	= {Jim Grundy and Malcom Newey},

   publisher     = Springer,

   series	= LNCS,

   volume        = 1479,

   year		= 1998}

 @Proceedings{tphols99,

   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},

   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},

   editor	= {Bertot, Y. and Dowek, G. and Hirschowitz, A. and

                   Paulin, C. and Thery, L.},

   publisher     = Springer,

   series	= LNCS,

   volume        = 1690,

   year		= 1999}

 @Proceedings{tphols2000,

   title         = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000},

   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000},

   editor        = {J. Harrison and M. Aagaard},

   publisher     = Springer,

   series        = LNCS,

   volume        = 1869,

   year          = 2000}

 @Proceedings{tphols2001,

   title         = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},

   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},

   editor        = {R. J. Boulton and P. B. Jackson},

   publisher     = Springer,

   series        = LNCS,

   volume        = 2152,

   year          = 2001}

 @Proceedings{ijcar2006,

   title         = {Automated Reasoning: {IJCAR} 2006},

   booktitle     = {Automated Reasoning: {IJCAR} 2006},

   editor        = {U. Furbach and N. Shankar},

   publisher     = Springer,

   series        = LNCS,

   volume        = 4130,

   year          = 2006}

 @Proceedings{tphols2007,

   title         = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007},

   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007},

   editor        = {K. Schneider and J. Brandt},

   publisher     = Springer,

   series        = LNCS,

   volume        = 4732,

   year          = 2007}

 @Proceedings{tphols2008,

   title         = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},

   booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},

   publisher     = Springer,

   series        = LNCS,

   year          = 2008}

 %  editor        =

 %  volume        = 4732,

 @Proceedings{itp2010,

   title         = {Interactive Theorem Proving: {ITP}-10},

   booktitle     = {Interactive Theorem Proving: {ITP}-10},

   editor = "Matt Kaufmann and Lawrence Paulson",

   publisher     = Springer,

   series        = LNCS,

   year          = 2010}

 @unpublished{classes_modules,

   title         = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},

   author        = {Stefan Wehr et. al.}

 }