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