Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-src/manual.bib
author wenzelm
Mon, 10 May 1999 17:02:05 +0200
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}
wneuper/isa