doc-src/manual.bib
author wenzelm
Mon May 10 17:02:05 1999 +0200 (1999-05-10)
changeset 6626 a92d2b6e0626
parent 6624 e0914e542f00
child 6670 4921b1f8ff92
permissions -rw-r--r--
tuned;
     1 % BibTeX database for the Isabelle documentation
     2 %
     3 % Lawrence C Paulson $Id$
     4 
     5 %publishers
     6 @string{AP="Academic Press"}
     7 @string{CUP="Cambridge University Press"}
     8 @string{IEEE="{\sc ieee} Computer Society Press"}
     9 @string{LNCS="Lect.\ Notes in Comp.\ Sci."}
    10 @string{MIT="MIT Press"}
    11 @string{NH="North-Holland"}
    12 @string{Prentice="Prentice-Hall"}
    13 @string{PH="Prentice-Hall"}
    14 @string{Springer="Springer-Verlag"}
    15 
    16 %institutions
    17 @string{CUCL="Comp. Lab., Univ. Camb."}
    18 @string{Edinburgh="Dept. Comp. Sci., Univ. Edinburgh"}
    19 
    20 %journals
    21 @string{FAC="Formal Aspects Comput."}
    22 @string{JAR="J. Auto. Reas."}
    23 @string{JCS="J. Comput. Secur."}
    24 @string{JFP="J. Func. Prog."}
    25 @string{JLC="J. Logic and Comput."}
    26 @string{JLP="J. Logic Prog."}
    27 @string{JSC="J. Symb. Comput."}
    28 @string{JSL="J. Symb. Logic"}
    29 @string{SIGPLAN="{SIGPLAN} Notices"}
    30 
    31 %conferences
    32 @string{CADE="International Conference on Automated Deduction"}
    33 @string{POPL="Symposium on Principles of Programming Languages"}
    34 @string{TYPES="Types for Proofs and Programs"}
    35 
    36 
    37 %A
    38 
    39 @incollection{abramsky90,
    40   author	= {Samson Abramsky},
    41   title		= {The Lazy Lambda Calculus},
    42   pages		= {65-116},
    43   editor	= {David A. Turner},
    44   booktitle	= {Research Topics in Functional Programming},
    45   publisher	= {Addison-Wesley},
    46   year		= 1990}
    47 
    48 @Unpublished{abrial93,
    49   author	= {J. R. Abrial and G. Laffitte},
    50   title		= {Towards the Mechanization of the Proofs of some Classical
    51 		  Theorems of Set Theory},
    52   note		= {preprint},
    53   year		= 1993,
    54   month		= Feb}
    55 
    56 @incollection{aczel77,
    57   author	= {Peter Aczel},
    58   title		= {An Introduction to Inductive Definitions},
    59   pages		= {739-782},
    60   crossref	= {barwise-handbk}}
    61 
    62 @Book{aczel88,
    63   author	= {Peter Aczel},
    64   title		= {Non-Well-Founded Sets},
    65   publisher	= {CSLI},
    66   year		= 1988}
    67 
    68 @InProceedings{alf,
    69   author	= {Lena Magnusson and Bengt {Nordstr\"{o}m}},
    70   title		= {The {ALF} Proof Editor and Its Proof Engine},
    71   crossref	= {types93},
    72   pages		= {213-237}}
    73 
    74 @book{andrews86,
    75   author	= "Peter Andrews",
    76   title		= "An Introduction to Mathematical Logic and Type Theory: to Truth
    77 through Proof",
    78   publisher	= AP,
    79   series	= "Computer Science and Applied Mathematics",
    80   year		= 1986}
    81 
    82 %B
    83 
    84 @incollection{basin91,
    85   author	= {David Basin and Matt Kaufmann},
    86   title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
    87 		   Comparison}, 
    88   crossref	= {huet-plotkin91},
    89   pages		= {89-119}}
    90 
    91 
    92 @InProceedings{Berghofer-Wenzel:1999:TPHOL,
    93   author = 	 {Stefan Berghofer and Markus Wenzel},
    94   title = 	 {Inductive datatypes in {HOL} --- lessons learned in {F}ormal-{L}ogic {E}ngineering},
    95   booktitle = 	 {Theorem Proving in Higher Order Logics (TPHOLs'99)},
    96   series =	 LNCS,
    97   year =	 1999,
    98   publisher =	 Springer
    99 }
   100 
   101 @book{Bird-Wadler,author="Richard Bird and Philip Wadler",
   102 title="Introduction to Functional Programming",publisher=PH,year=1988}
   103 
   104 @Article{boyer86,
   105   author	= {Robert Boyer and Ewing Lusk and William McCune and Ross
   106 		   Overbeek and Mark Stickel and Lawrence Wos},
   107   title		= {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}
   108 		   Axioms},
   109   journal	= JAR,
   110   year		= 1986,
   111   volume	= 2,
   112   number	= 3,
   113   pages		= {287-327}}
   114 
   115 @book{bm79,
   116   author	= {Robert S. Boyer and J Strother Moore},
   117   title		= {A Computational Logic},
   118   publisher	= {Academic Press},
   119   year		= 1979}
   120 
   121 @book{bm88book,
   122   author	= {Robert S. Boyer and J Strother Moore},
   123   title		= {A Computational Logic Handbook},
   124   publisher	= {Academic Press},
   125   year		= 1988}
   126 
   127 @Article{debruijn72,
   128   author	= {N. G. de Bruijn},
   129   title		= {Lambda Calculus Notation with Nameless Dummies,
   130 	a Tool for Automatic Formula Manipulation,
   131 	with Application to the {Church-Rosser Theorem}},
   132   journal	= {Indag. Math.},
   133   volume	= 34,
   134   pages		= {381-392},
   135   year		= 1972}
   136 
   137 %C
   138 
   139 @TechReport{camilleri92,
   140   author	= {J. Camilleri and T. F. Melham},
   141   title		= {Reasoning with Inductively Defined Relations in the
   142 		 {HOL} Theorem Prover},
   143   institution	= CUCL,
   144   year		= 1992,
   145   number	= 265,
   146   month		= Aug}
   147 
   148 @Book{charniak80,
   149   author	= {E. Charniak and C. K. Riesbeck and D. V. McDermott},
   150   title		= {Artificial Intelligence Programming},
   151   publisher	= {Lawrence Erlbaum Associates},
   152   year		= 1980}
   153 
   154 @article{church40,
   155   author	= "Alonzo Church",
   156   title		= "A Formulation of the Simple Theory of Types",
   157   journal	= JSL,
   158   year		= 1940,
   159   volume	= 5,
   160   pages		= "56-68"}
   161 
   162 @PhdThesis{coen92,
   163   author	= {Martin D. Coen},
   164   title		= {Interactive Program Derivation},
   165   school	= {University of Cambridge},
   166   note		= {Computer Laboratory Technical Report 272},
   167   month		= nov,
   168   year		= 1992}
   169 
   170 @book{constable86,
   171   author	= {R. L. Constable and others},
   172   title		= {Implementing Mathematics with the Nuprl Proof
   173 		 Development System}, 
   174   publisher	= Prentice,
   175   year		= 1986}
   176 
   177 %D
   178 
   179 @Book{davey&priestley,
   180   author	= {B. A. Davey and H. A. Priestley},
   181   title		= {Introduction to Lattices and Order},
   182   publisher	= CUP,
   183   year		= 1990}
   184 
   185 @Book{devlin79,
   186   author	= {Keith J. Devlin},
   187   title		= {Fundamentals of Contemporary Set Theory},
   188   publisher	= {Springer},
   189   year		= 1979}
   190 
   191 @book{dummett,
   192   author	= {Michael Dummett},
   193   title		= {Elements of Intuitionism},
   194   year		= 1977,
   195   publisher	= {Oxford University Press}}
   196 
   197 @incollection{dybjer91,
   198   author	= {Peter Dybjer},
   199   title		= {Inductive Sets and Families in {Martin-L\"of's} Type
   200 		  Theory and Their Set-Theoretic Semantics}, 
   201   crossref	= {huet-plotkin91},
   202   pages		= {280-306}}
   203 
   204 @Article{dyckhoff,
   205   author	= {Roy Dyckhoff},
   206   title		= {Contraction-Free Sequent Calculi for Intuitionistic Logic},
   207   journal	= JSL,
   208   year		= 1992,
   209   volume	= 57,
   210   number	= 3,
   211   pages		= {795-807}}
   212 
   213 %F
   214 
   215 @Article{IMPS,
   216   author	= {William M. Farmer and Joshua D. Guttman and F. Javier
   217 		 Thayer},
   218   title		= {{IMPS}: An Interactive Mathematical Proof System},
   219   journal	= JAR,
   220   volume	= 11,
   221   number	= 2,
   222   year		= 1993,
   223   pages		= {213-248}}
   224 
   225 @InProceedings{felty91a,
   226   Author	= {Amy Felty},
   227   Title		= {A Logic Program for Transforming Sequent Proofs to Natural
   228 		  Deduction Proofs}, 
   229   crossref	= {extensions91},
   230   pages		= {157-178}}
   231 
   232 @TechReport{frost93,
   233   author	= {Jacob Frost},
   234   title		= {A Case Study of Co-induction in {Isabelle HOL}},
   235   institution	= CUCL,
   236   number	= 308,
   237   year		= 1993,
   238   month		= Aug}
   239 
   240 %revised version of frost93
   241 @TechReport{frost95,
   242   author	= {Jacob Frost},
   243   title		= {A Case Study of Co-induction in {Isabelle}},
   244   institution	= CUCL,
   245   number	= 359,
   246   year		= 1995,
   247   month		= Feb}
   248 
   249 @inproceedings{OBJ,
   250   author	= {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
   251 		 and J. Meseguer}, 
   252   title		= {Principles of {OBJ2}},
   253   booktitle	= POPL, 
   254   year		= 1985,
   255   pages		= {52-66}}
   256 
   257 %G
   258 
   259 @book{gallier86,
   260   author	= {J. H. Gallier},
   261   title		= {Logic for Computer Science: 
   262 		Foundations of Automatic Theorem Proving},
   263   year		= 1986,
   264   publisher	= {Harper \& Row}}
   265 
   266 @Book{galton90,
   267   author	= {Antony Galton},
   268   title		= {Logic for Information Technology},
   269   publisher	= {Wiley},
   270   year		= 1990}
   271 
   272 @InProceedings{gimenez-codifying,
   273   author	= {Eduardo Gim{\'e}nez},
   274   title		= {Codifying Guarded Definitions with Recursive Schemes},
   275   crossref	= {types94},
   276   pages		= {39-59}
   277 }
   278 
   279 @Book{mgordon-hol,
   280   author	= {M. J. C. Gordon and T. F. Melham},
   281   title		= {Introduction to {HOL}: A Theorem Proving Environment for
   282 		 Higher Order Logic},
   283   publisher	= CUP,
   284   year		= 1993}
   285 
   286 @book{mgordon79,
   287   author	= {Michael J. C. Gordon and Robin Milner and Christopher P.
   288 		 Wadsworth},
   289   title		= {Edinburgh {LCF}: A Mechanised Logic of Computation},
   290   year		= 1979,
   291   publisher	= {Springer},
   292   series	= {LNCS 78}}
   293 
   294 @inproceedings{Gunter-HOL92,author={Elsa L. Gunter},
   295 title={Why we can't have {SML} style datatype declarations in {HOL}},
   296 booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.\
   297 IFIP TC10/WG10.2 Intl. Workshop, 1992},
   298 editor={L.J.M. Claesen and M.J.C. Gordon},
   299 publisher=NH,year=1993,pages={561--568}}
   300 
   301 @InProceedings{gunter-trees,
   302   author	= {Elsa L. Gunter},
   303   title		= {A Broader Class of Trees for Recursive Type Definitions for
   304 		  {HOL}},
   305   crossref	= {hug93},
   306   pages		= {141-154}}
   307 
   308 %H
   309 
   310 @Book{halmos60,
   311   author	= {Paul R. Halmos},
   312   title		= {Naive Set Theory},
   313   publisher	= {Van Nostrand},
   314   year		= 1960}
   315 
   316 @Book{hennessy90,
   317   author	= {Matthew Hennessy},
   318   title		= {The Semantics of Programming Languages: An Elementary
   319 		  Introduction Using Structural Operational Semantics},
   320   publisher	= {Wiley},
   321   year		= 1990}
   322 
   323 @Article{haskell-report,
   324   author	= {Paul Hudak and Simon Peyton Jones and Philip Wadler},
   325   title		= {Report on the Programming Language {Haskell}: A
   326 		 Non-strict, Purely Functional Language},
   327   journal	= SIGPLAN,
   328   year		= 1992,
   329   volume	= 27,
   330   number	= 5,
   331   month		= May,
   332   note		= {Version 1.2}}
   333 
   334 @Article{haskell-tutorial,
   335   author	= {Paul Hudak and Joseph H. Fasel},
   336   title		= {A Gentle Introduction to {Haskell}},
   337   journal	= SIGPLAN,
   338   year		= 1992,
   339   volume	= 27,
   340   number	= 5,
   341   month		= May}
   342 
   343 @article{huet75,
   344   author	= {G. P. Huet},
   345   title		= {A Unification Algorithm for Typed $\lambda$-Calculus},
   346   journal	= TCS,
   347   volume	= 1,
   348   year		= 1975,
   349   pages		= {27-57}}
   350 
   351 @article{huet78,
   352   author	= {G. P. Huet and B. Lang},
   353   title		= {Proving and Applying Program Transformations Expressed with 
   354 			Second-Order Patterns},
   355   journal	= acta,
   356   volume	= 11,
   357   year		= 1978, 
   358   pages		= {31-55}}
   359 
   360 @inproceedings{huet88,
   361   author	= {G\'erard Huet},
   362   title		= {Induction Principles Formalized in the {Calculus of
   363 		 Constructions}}, 
   364   booktitle	= {Programming of Future Generation Computers},
   365   editor	= {K. Fuchi and M. Nivat},
   366   year		= 1988,
   367   pages		= {205-216}, 
   368   publisher	= {Elsevier}}
   369 
   370 %K
   371 
   372 @book{Knuth3-75,author={Donald E. Knuth},
   373 title={The Art of Computer Programming, Volume 3: Sorting and Searching},
   374 publisher={Addison-Wesley},year=1975}
   375 
   376 @Book{kunen80,
   377   author	= {Kenneth Kunen},
   378   title		= {Set Theory: An Introduction to Independence Proofs},
   379   publisher	= NH,
   380   year		= 1980}
   381 
   382 %M
   383 
   384 @Article{mw81,
   385   author	= {Zohar Manna and Richard Waldinger},
   386   title		= {Deductive Synthesis of the Unification Algorithm},
   387   journal	= SCP,
   388   year		= 1981,
   389   volume	= 1,
   390   number	= 1,
   391   pages		= {5-48}}
   392 
   393 @InProceedings{martin-nipkow,
   394   author	= {Ursula Martin and Tobias Nipkow},
   395   title		= {Ordered Rewriting and Confluence},
   396   crossref	= {cade10},
   397   pages		= {366-380}}
   398 
   399 @book{martinlof84,
   400   author	= {Per Martin-L\"of},
   401   title		= {Intuitionistic type theory},
   402   year		= 1984,
   403   publisher	= {Bibliopolis}}
   404 
   405 @incollection{melham89,
   406   author	= {Thomas F. Melham},
   407   title		= {Automating Recursive Type Definitions in Higher Order
   408 		 Logic}, 
   409   pages		= {341-386},
   410   crossref	= {birtwistle89}}
   411 
   412 @Article{miller-mixed,
   413   Author	= {Dale Miller},
   414   Title		= {Unification Under a Mixed Prefix},
   415   journal	= JSC,
   416   volume	= 14,
   417   number	= 4,
   418   pages		= {321-358},
   419   Year		= 1992}
   420 
   421 @Article{milner78,
   422   author	= {Robin Milner},
   423   title		= {A Theory of Type Polymorphism in Programming},
   424   journal	= "J. Comp.\ Sys.\ Sci.",
   425   year		= 1978,
   426   volume	= 17,
   427   pages		= {348-375}}
   428 
   429 @TechReport{milner-ind,
   430   author	= {Robin Milner},
   431   title		= {How to Derive Inductions in {LCF}},
   432   institution	= Edinburgh,
   433   year		= 1980,
   434   type		= {note}}
   435 
   436 @Article{milner-coind,
   437   author	= {Robin Milner and Mads Tofte},
   438   title		= {Co-induction in Relational Semantics},
   439   journal	= TCS,
   440   year		= 1991,
   441   volume	= 87,
   442   pages		= {209-220}}
   443 
   444 @Book{milner89,
   445   author	= {Robin Milner},
   446   title		= {Communication and Concurrency},
   447   publisher	= Prentice,
   448   year		= 1989}
   449 
   450 @PhdThesis{monahan84,
   451   author	= {Brian Q. Monahan},
   452   title		= {Data Type Proofs using Edinburgh {LCF}},
   453   school	= {University of Edinburgh},
   454   year		= 1984}
   455 
   456 @article{MuellerNvOS99,
   457 author=
   458 {Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oskar Slotosch},
   459 title={{HOLCF = HOL + LCF}},journal=JFP,year=1999}
   460 
   461 %N
   462 
   463 @InProceedings{NaraschewskiW-TPHOLs98,
   464   author	= {Wolfgang Naraschewski and Markus Wenzel},
   465   title		= 
   466 {Object-Oriented Verification based on Record Subtyping in Higher-Order Logic},
   467   booktitle	= {Theorem Proving in Higher Order Logics (TPHOLs'98)},
   468   publisher	= Springer,
   469   volume	= 1479,
   470   series	= LNCS,
   471   year		= 1998}
   472 
   473 @inproceedings{nazareth-nipkow,
   474   author	= {Dieter Nazareth and Tobias Nipkow},
   475   title		= {Formal Verification of Algorithm {W}: The Monomorphic Case},
   476   crossref	= {tphols96},
   477   pages		= {331-345},
   478   year		= 1996}
   479 
   480 @inproceedings{nipkow-W,
   481   author	= {Wolfgang Naraschewski and Tobias Nipkow},
   482   title		= {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
   483   booktitle	= {Types for Proofs and Programs: Intl. Workshop TYPES '96},
   484   editor	= {E. Gim\'enez and C. Paulin-Mohring},
   485   publisher	= Springer,
   486   series	= LNCS,
   487   volume	= 1512,
   488   pages		= {317-332},
   489   year		= 1998}
   490 
   491 @inproceedings{Nipkow-CR,
   492   author	= {Tobias Nipkow},
   493   title		= {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
   494   booktitle	= {Automated Deduction --- CADE-13},
   495   editor	= {M. McRobbie and J.K. Slaney},
   496   publisher	= Springer,
   497   series	= LNCS,
   498   volume	= 1104,
   499   pages		= {733-747},
   500   year		= 1996}
   501 
   502 % WAS Nipkow-LICS-93
   503 @InProceedings{nipkow-patterns,
   504   title		= {Functional Unification of Higher-Order Patterns},
   505   author	= {Tobias Nipkow},
   506   pages		= {64-74},
   507   crossref	= {lics8},
   508   url		= {ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html},
   509   keywords	= {unification}}
   510 
   511 @article{nipkow-IMP,
   512   author	= {Tobias Nipkow},
   513   title		= {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
   514   journal	= FAC,
   515   volume	= 10,
   516   pages		= {171-186},
   517   year		= 1998}
   518 
   519 @manual{isabelle-HOL,
   520   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
   521   title		= {{Isabelle}'s Logics: {HOL}},
   522   institution	= {Institut f\"ur Informatik, Technische Universi\"at
   523                   M\"unchen and Computer Laboratory, University of Cambridge}}
   524 
   525 @article{nipkow-prehofer,
   526   author	= {Tobias Nipkow and Christian Prehofer},
   527   title		= {Type Reconstruction for Type Classes},
   528   journal	= JFP,
   529   volume	= 5,
   530   number	= 2,
   531   year		= 1995,
   532   pages		= {201-224}}
   533 
   534 @Article{noel,
   535   author	= {Philippe No{\"e}l},
   536   title		= {Experimenting with {Isabelle} in {ZF} Set Theory},
   537   journal	= JAR,
   538   volume	= 10,
   539   number	= 1,
   540   pages		= {15-58},
   541   year		= 1993}
   542 
   543 @book{nordstrom90,
   544   author	= {Bengt {Nordstr\"om} and Kent Petersson and Jan Smith},
   545   title		= {Programming in {Martin-L\"of}'s Type Theory.  An
   546 		 Introduction}, 
   547   publisher	= {Oxford University Press}, 
   548   year		= 1990}
   549 
   550 %O
   551 
   552 @Manual{pvs-language,
   553   title		= {The {PVS} specification language},
   554   author	= {S. Owre and N. Shankar and J. M. Rushby},
   555   organization	= {Computer Science Laboratory, SRI International},
   556   address	= {Menlo Park, CA},
   557   note		= {Beta release},
   558   year		= 1993,
   559   month		= apr,
   560   url		= {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}}
   561 
   562 %P
   563 
   564 % replaces paulin92
   565 @InProceedings{paulin-tlca,
   566   author	= {Christine Paulin-Mohring},
   567   title		= {Inductive Definitions in the System {Coq}: Rules and
   568 		 Properties},
   569   crossref	= {tlca93},
   570   pages		= {328-345}}
   571 
   572 @InProceedings{paulson-CADE,
   573   author	= {Lawrence C. Paulson},
   574   title		= {A Fixedpoint Approach to Implementing (Co)Inductive
   575 		  Definitions},
   576   pages		= {148-161},
   577   crossref	= {cade12}}
   578 
   579 @InProceedings{paulson-COLOG,
   580   author	= {Lawrence C. Paulson},
   581   title		= {A Formulation of the Simple Theory of Types (for
   582 		 {Isabelle})}, 
   583   pages		= {246-274},
   584   crossref	= {colog88},
   585   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}}
   586 
   587 @Article{paulson-coind,
   588   author	= {Lawrence C. Paulson},
   589   title		= {Mechanizing Coinduction and Corecursion in Higher-Order
   590 		  Logic},
   591   journal	= JLC,
   592   year		= 1997,
   593   volume	= 7,
   594   number	= 2,
   595   month		= mar,
   596   pages		= {175-204}}
   597 
   598 @manual{isabelle-ref,
   599   author	= {Lawrence C. Paulson},
   600   title		= {The {Isabelle} Reference Manual},
   601   institution	= CUCL}
   602 
   603 @manual{isabelle-ZF,
   604   author	= {Lawrence C. Paulson},
   605   title		= {{Isabelle}'s Logics: {FOL} and {ZF}},
   606   institution	= CUCL}
   607 
   608 @article{paulson-found,
   609   author	= {Lawrence C. Paulson},
   610   title		= {The Foundation of a Generic Theorem Prover},
   611   journal	= JAR,
   612   volume	= 5,
   613   number	= 3,
   614   pages		= {363-397},
   615   year		= 1989,
   616   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}}
   617 
   618 %replaces paulson-final
   619 @Article{paulson-mscs,
   620   author	= {Lawrence C. Paulson},
   621   title		= {Final Coalgebras as Greatest Fixed Points in ZF Set Theory},
   622   journal	= {Mathematical Structures in Computer Science},
   623   year		= 1999,
   624   volume	= 9,
   625   note		= {in press}}
   626 
   627 @InCollection{paulson-generic,
   628   author	= {Lawrence C. Paulson},
   629   title		= {Generic Automatic Proof Tools},
   630   crossref	= {wos-fest},
   631   chapter	= 3}
   632 
   633 @Article{paulson-gr,
   634   author	= {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
   635   title		= {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of
   636 		  Choice},
   637   journal	= JAR,
   638   year		= 1996,
   639   volume	= 17,
   640   number	= 3,
   641   month		= dec,
   642   pages		= {291-323}}
   643 
   644 @InCollection{paulson-handbook,
   645   author	= {Lawrence C. Paulson},
   646   title		= {Designing a Theorem Prover},
   647   crossref	= {handbk-lics2},
   648   pages		= {415-475}}
   649 
   650 @Book{paulson-isa-book,
   651   author	= {Lawrence C. Paulson},
   652   title		= {Isabelle: A Generic Theorem Prover},
   653   publisher	= {Springer},
   654   year		= 1994,
   655   note		= {LNCS 828}}
   656 
   657 @InCollection{paulson-markt,
   658   author	= {Lawrence C. Paulson},
   659   title		= {Tool Support for Logics of Programs},
   660   booktitle	= {Mathematical Methods in Program Development:
   661                   Summer School Marktoberdorf 1996},
   662   publisher	= {Springer},
   663   pages		= {461-498},
   664   year		= {Published 1997},
   665   editor	= {Manfred Broy},
   666   series	= {NATO ASI Series F}}
   667 
   668 %replaces Paulson-ML and paulson91
   669 @book{paulson-ml2,
   670   author	= {Lawrence C. Paulson},
   671   title		= {{ML} for the Working Programmer},
   672   year		= 1996,
   673   edition	= {2nd},
   674   publisher	= CUP}
   675 
   676 @article{paulson-natural,
   677   author	= {Lawrence C. Paulson},
   678   title		= {Natural Deduction as Higher-order Resolution},
   679   journal	= JLP,
   680   volume	= 3,
   681   pages		= {237-258},
   682   year		= 1986,
   683   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}}
   684 
   685 @Article{paulson-set-I,
   686   author	= {Lawrence C. Paulson},
   687   title		= {Set Theory for Verification: {I}.  {From}
   688 		 Foundations to Functions},
   689   journal	= JAR,
   690   volume	= 11,
   691   number	= 3,
   692   pages		= {353-389},
   693   year		= 1993,
   694   url		= {ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}
   695 
   696 @Article{paulson-set-II,
   697   author	= {Lawrence C. Paulson},
   698   title		= {Set Theory for Verification: {II}.  {Induction} and
   699 		 Recursion},
   700   journal	= JAR,
   701   volume	= 15,
   702   number	= 2,
   703   pages		= {167-215},
   704   year		= 1995,
   705   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}}
   706 
   707 @article{paulson85,
   708   author	= {Lawrence C. Paulson},
   709   title		= {Verifying the Unification Algorithm in {LCF}},
   710   journal	= SCP,
   711   volume	= 5,
   712   pages		= {143-170},
   713   year		= 1985}
   714 
   715 %replqces Paulson-LCF
   716 @book{paulson87,
   717   author	= {Lawrence C. Paulson},
   718   title		= {Logic and Computation: Interactive proof with Cambridge
   719 		 LCF}, 
   720   year		= 1987,
   721   publisher	= CUP}
   722 
   723 @incollection{paulson700,
   724   author	= {Lawrence C. Paulson},
   725   title		= {{Isabelle}: The Next 700 Theorem Provers},
   726   crossref	= {odifreddi90},
   727   pages		= {361-386},
   728   url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}}
   729 
   730 % replaces paulson-ns and paulson-security
   731 @Article{paulson-jcs,
   732   author	= {Lawrence C. Paulson},
   733   title		= {The Inductive Approach to Verifying Cryptographic Protocols},
   734   journal	= JCS,
   735   year		= 1998,
   736   volume	= 6,
   737   pages		= {85-128}}
   738 
   739 @article{pelletier86,
   740   author	= {F. J. Pelletier},
   741   title		= {Seventy-five Problems for Testing Automatic Theorem
   742 		 Provers}, 
   743   journal	= JAR,
   744   volume	= 2,
   745   pages		= {191-216},
   746   year		= 1986,
   747   note		= {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}}
   748 
   749 @Article{pitts94,  
   750   author	= {Andrew M. Pitts},
   751   title		= {A Co-induction Principle for Recursively Defined Domains},
   752   journal	= TCS,
   753   volume	= 124, 
   754   pages		= {195-219},
   755   year		= 1994} 
   756 
   757 @Article{plaisted90,
   758   author	= {David A. Plaisted},
   759   title		= {A Sequent-Style Model Elimination Strategy and a Positive
   760 		 Refinement},
   761   journal	= JAR,
   762   year		= 1990,
   763   volume	= 6,
   764   number	= 4,
   765   pages		= {389-402}}
   766 
   767 %Q
   768 
   769 @Article{quaife92,
   770   author	= {Art Quaife},
   771   title		= {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set
   772 		 Theory},
   773   journal	= JAR,
   774   year		= 1992,
   775   volume	= 8,
   776   number	= 1,
   777   pages		= {91-147}}
   778 
   779 %R
   780 
   781 @TechReport{rasmussen95,
   782   author	= {Ole Rasmussen},
   783   title		= {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting
   784 		  Experiment},
   785   institution	= {Computer Laboratory, University of Cambridge},
   786   year		= 1995,
   787   number	= 364,
   788   month		= may,
   789   url		= {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}}
   790 
   791 @Book{reeves90,
   792   author	= {Steve Reeves and Michael Clarke},
   793   title		= {Logic for Computer Science},
   794   publisher	= {Addison-Wesley},
   795   year		= 1990}
   796 
   797 %S
   798 
   799 @inproceedings{saaltink-fme,
   800   author	= {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
   801 		 Dan Craigen and Irwin Meisels},
   802   title		= {An {EVES} Data Abstraction Example}, 
   803   pages		= {578-596},
   804   crossref	= {fme93}}
   805 
   806 @inproceedings{slind-tfl,
   807   author	= {Konrad Slind},
   808   title		= {Function Definition in Higher Order Logic},
   809   booktitle	= {Theorem Proving in Higher Order Logics},
   810   editor	= {J. von Wright and J. Grundy and J. Harrison},
   811   publisher	= Springer,
   812   series	= LNCS,
   813   volume	= 1125,
   814   pages		= {381-397},
   815   year		= 1996}
   816 
   817 @book{suppes72,
   818   author	= {Patrick Suppes},
   819   title		= {Axiomatic Set Theory},
   820   year		= 1972,
   821   publisher	= {Dover}}
   822 
   823 @InCollection{szasz93,
   824   author	= {Nora Szasz},
   825   title		= {A Machine Checked Proof that {Ackermann's} Function is not
   826 		  Primitive Recursive},
   827   crossref	= {huet-plotkin93},
   828   pages		= {317-338}}
   829 
   830 %T
   831 
   832 @book{takeuti87,
   833   author	= {G. Takeuti},
   834   title		= {Proof Theory},
   835   year		= 1987,
   836   publisher	= NH,
   837   edition	= {2nd}}
   838 
   839 @Book{thompson91,
   840   author	= {Simon Thompson},
   841   title		= {Type Theory and Functional Programming},
   842   publisher	= {Addison-Wesley},
   843   year		= 1991}
   844 
   845 %V
   846 
   847 @Unpublished{voelker94,
   848   author	= {Norbert V\"olker},
   849   title		= {The Verification of a Timer Program using {Isabelle/HOL}},
   850   url		= {ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz},
   851   year		= 1994,
   852   month		= aug}
   853 
   854 %W
   855 
   856 
   857 @InProceedings{Wenzel:1997:TPHOL,
   858   author = 	 {Markus Wenzel},
   859   title = 	 {Type Classes and Overloading in Higher-Order Logic},
   860   booktitle = 	 {Theorem Proving in Higher Order Logics (TPHOLs'97)},
   861   year =	 1997,
   862   series =	 LNCS,
   863   volume =       1275,
   864   publisher =	 Springer
   865 }
   866 
   867 @book{principia,
   868   author	= {A. N. Whitehead and B. Russell},
   869   title		= {Principia Mathematica},
   870   year		= 1962,
   871   publisher	= CUP, 
   872   note		= {Paperback edition to *56,
   873   abridged from the 2nd edition (1927)}}
   874 
   875 @book{winskel93,
   876   author	= {Glynn Winskel},
   877   title		= {The Formal Semantics of Programming Languages},
   878   publisher	= MIT,year=1993}
   879 
   880 @InCollection{wos-bledsoe,
   881   author	= {Larry Wos},
   882   title		= {Automated Reasoning and {Bledsoe's} Dream for the Field},
   883   crossref	= {bledsoe-fest},
   884   pages		= {297-342}}
   885 
   886 
   887 % CROSS REFERENCES
   888 
   889 @book{handbk-lics2,
   890   editor	= {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
   891   title		= {Handbook of Logic in Computer Science},
   892   booktitle	= {Handbook of Logic in Computer Science},
   893   publisher	= {Oxford University Press},
   894   year		= 1992,
   895   volume	= 2}
   896 
   897 @book{types93,
   898   editor	= {Henk Barendregt and Tobias Nipkow},
   899   title		= TYPES # {: International Workshop {TYPES '93}},
   900   booktitle	= TYPES # {: International Workshop {TYPES '93}},
   901   year		= {published 1994},
   902   publisher	= {Springer},
   903   series	= {LNCS 806}}
   904 
   905 @book{barwise-handbk,
   906   editor	= {J. Barwise},
   907   title		= {Handbook of Mathematical Logic},
   908   booktitle	= {Handbook of Mathematical Logic},
   909   year		= 1977,
   910   publisher	= NH}
   911 
   912 @Proceedings{tlca93,
   913   title		= {Typed Lambda Calculi and Applications},
   914   booktitle	= {Typed Lambda Calculi and Applications},
   915   editor	= {M. Bezem and J.F. Groote},
   916   year		= 1993,
   917   publisher	= {Springer},
   918   series	= {LNCS 664}}
   919 
   920 @book{birtwistle89,
   921   editor	= {Graham Birtwistle and P. A. Subrahmanyam},
   922   title		= {Current Trends in Hardware Verification and Automated
   923 		 Theorem Proving}, 
   924   booktitle	= {Current Trends in Hardware Verification and Automated
   925 		 Theorem Proving}, 
   926   publisher	= {Springer},
   927   year		= 1989}
   928 
   929 @book{bledsoe-fest,
   930   title		= {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
   931   booktitle	= {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
   932   publisher	= {Kluwer Academic Publishers},
   933   year		= 1991,
   934   editor	= {Robert S. Boyer}}
   935 
   936 @Proceedings{cade12,
   937   editor	= {Alan Bundy},
   938   title		= {Automated Deduction --- {CADE}-12 
   939 		  International Conference},
   940   booktitle	= {Automated Deduction --- {CADE}-12 
   941 		  International Conference},
   942   year		= 1994,
   943   series	= {LNAI 814},
   944   publisher	= {Springer}}
   945 
   946 @book{types94,
   947   editor	= {Peter Dybjer and Bengt Nordstr{\"om} and Jan Smith},
   948   title		= TYPES # {: International Workshop {TYPES '94}},
   949   booktitle	= TYPES # {: International Workshop {TYPES '94}},
   950   year		= 1995,
   951   publisher	= {Springer},
   952   series	= {LNCS 996}}
   953 
   954 @book{huet-plotkin91,
   955   editor	= {{G\'erard} Huet and Gordon Plotkin},
   956   title		= {Logical Frameworks},
   957   booktitle	= {Logical Frameworks},
   958   publisher	= CUP,
   959   year		= 1991}
   960 
   961 @book{huet-plotkin93,
   962   editor	= {{G\'erard} Huet and Gordon Plotkin},
   963   title		= {Logical Environments},
   964   booktitle	= {Logical Environments},
   965   publisher	= CUP,
   966   year		= 1993}
   967 
   968 @Proceedings{hug93,
   969   editor	= {J. Joyce and C. Seger},
   970   title		= {Higher Order Logic Theorem Proving and Its
   971 		  Applications: HUG '93},
   972   booktitle	= {Higher Order Logic Theorem Proving and Its
   973 		  Applications: HUG '93},
   974   year		= {Published 1994},
   975   publisher	= {Springer},
   976   series	= {LNCS 780}}
   977 
   978 @proceedings{colog88,
   979   editor	= {P. Martin-L\"of and G. Mints},
   980   title		= {COLOG-88: International Conference on Computer Logic},
   981   booktitle	= {COLOG-88: International Conference on Computer Logic},
   982   year		= {Published 1990},
   983   publisher	= {Springer},
   984   organization	= {Estonian Academy of Sciences},
   985   address	= {Tallinn},
   986   series	= {LNCS 417}}
   987 
   988 @book{odifreddi90,
   989   editor	= {P. Odifreddi},
   990   title		= {Logic and Computer Science},
   991   booktitle	= {Logic and Computer Science},
   992   publisher	= {Academic Press},
   993   year		= 1990}
   994 
   995 @proceedings{extensions91,
   996   editor	= {Peter Schroeder-Heister},
   997   title		= {Extensions of Logic Programming},
   998   booktitle	= {Extensions of Logic Programming},
   999   year		= 1991,
  1000   series	= {LNAI 475}, 
  1001   publisher	= {Springer}}
  1002 
  1003 @proceedings{cade10,
  1004   editor	= {Mark E. Stickel},
  1005   title		= {10th } # CADE,
  1006   booktitle	= {10th } # CADE,
  1007   year		= 1990,
  1008   publisher	= {Springer},
  1009   series	= {LNAI 449}}
  1010 
  1011 @Proceedings{lics8,
  1012   editor	= {M. Vardi},
  1013   title		= {Eighth Annual Symposium on Logic in Computer Science},
  1014   booktitle	= {Eighth Annual Symposium on Logic in Computer Science},
  1015   publisher	= IEEE,
  1016   year		= 1993}
  1017 
  1018 @book{wos-fest,
  1019   title		= {Automated Reasoning and its Applications: 
  1020 			Essays in Honor of {Larry Wos}},
  1021   booktitle	= {Automated Reasoning and its Applications: 
  1022 			Essays in Honor of {Larry Wos}},
  1023   publisher	= {MIT Press},
  1024   year		= 1997,
  1025   editor	= {Robert Veroff}}
  1026 
  1027 @proceedings{fme93,
  1028   editor	= {J. C. P. Woodcock and P. G. Larsen},
  1029   title		= {FME '93: Industrial-Strength Formal Methods},
  1030   booktitle	= {FME '93: Industrial-Strength Formal Methods},
  1031   year		= 1993,
  1032   publisher	= {Springer},
  1033   series	= {LNCS 670}}
  1034 
  1035 @Proceedings{tphols96,
  1036   title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
  1037   booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
  1038   editor	= {J. von Wright and J. Grundy and J. Harrison},
  1039   series	= {LNCS 1125},
  1040   year		= 1996}