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