--- a/doc-src/HOL/logics-HOL.bbl Wed May 05 14:31:31 1999 +0200
+++ b/doc-src/HOL/logics-HOL.bbl Wed May 05 16:44:42 1999 +0200
@@ -1,34 +1,15 @@
\begin{thebibliography}{10}
\bibitem{andrews86}
-Peter~B. Andrews.
-\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
- Through Proof}.
-\newblock Academic Press, 1986.
+Peter Andrews.
+\newblock {\em An Introduction to Mathematical Logic and Type Theory: to Truth
+ through Proof}.
+\newblock Computer Science and Applied Mathematics. Academic Press, 1986.
\bibitem{church40}
Alonzo Church.
\newblock A formulation of the simple theory of types.
-\newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.
-
-\bibitem{coen92}
-Martin~D. Coen.
-\newblock {\em Interactive Program Derivation}.
-\newblock PhD thesis, University of Cambridge, November 1992.
-\newblock Computer Laboratory Technical Report 272.
-
-\bibitem{constable86}
-R.~L. Constable et~al.
-\newblock {\em Implementing Mathematics with the Nuprl Proof Development
- System}.
-\newblock Prentice-Hall, 1986.
-
-\bibitem{felty91a}
-Amy Felty.
-\newblock A logic program for transforming sequent proofs to natural deduction
- proofs.
-\newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic
- Programming}, LNAI 475, pages 157--178. Springer, 1991.
+\newblock {\em J. Symb. Logic}, 5:56--68, 1940.
\bibitem{frost93}
Jacob Frost.
@@ -36,92 +17,58 @@
\newblock Technical Report 308, Computer Laboratory, University of Cambridge,
August 1993.
-\bibitem{gallier86}
-J.~H. Gallier.
-\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
- Proving}.
-\newblock Harper \& Row, 1986.
-
\bibitem{mgordon-hol}
M.~J.~C. Gordon and T.~F. Melham.
\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
Order Logic}.
\newblock Cambridge University Press, 1993.
-\bibitem{huet78}
-G.~P. Huet and B.~Lang.
-\newblock Proving and applying program transformations expressed with
- second-order patterns.
-\newblock {\em Acta Informatica}, 11:31--55, 1978.
-
-\bibitem{alf}
-Lena Magnusson and Bengt {Nordstr\"{o}m}.
-\newblock The {ALF} proof editor and its proof engine.
-\newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs
- and Programs: International Workshop {TYPES '93}}, LNCS 806, pages 213--237.
- Springer, published 1994.
-
\bibitem{mw81}
Zohar Manna and Richard Waldinger.
\newblock Deductive synthesis of the unification algorithm.
\newblock {\em Science of Computer Programming}, 1(1):5--48, 1981.
-\bibitem{martinlof84}
-Per Martin-L\"of.
-\newblock {\em Intuitionistic type theory}.
-\newblock Bibliopolis, 1984.
-
\bibitem{milner78}
Robin Milner.
\newblock A theory of type polymorphism in programming.
-\newblock {\em Journal of Computer and System Sciences}, 17:348--375, 1978.
+\newblock {\em J. Comp.\ Sys.\ Sci.}, 17:348--375, 1978.
\bibitem{milner-coind}
Robin Milner and Mads Tofte.
\newblock Co-induction in relational semantics.
\newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
-\bibitem{Naraschewski-Wenzel:1998:TPHOL}
+\bibitem{nipkow-W}
+Wolfgang Naraschewski and Tobias Nipkow.
+\newblock Type inference verified: Algorithm {W} in {Isabelle/HOL}.
+\newblock In E.~Gim\'enez and C.~Paulin-Mohring, editors, {\em Types for Proofs
+ and Programs: Intl. Workshop TYPES '96}, volume 1512 of {\em Lect.\ Notes in
+ Comp.\ Sci.}, pages 317--332. Springer-Verlag, 1998.
+
+\bibitem{NaraschewskiW-TPHOLs98}
Wolfgang Naraschewski and Markus Wenzel.
\newblock Object-oriented verification based on record subtyping in
higher-order logic.
-\newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in
- Higher Order Logics: {TPHOLs} '98}, LNCS 1479, pages 349--366, 1998.
-
-\bibitem{nazareth-nipkow}
-Dieter Nazareth and Tobias Nipkow.
-\newblock Formal verification of algorithm {W}: The monomorphic case.
-\newblock In von Wright et~al. \cite{tphols96}, pages 331--345.
+\newblock In {\em Theorem Proving in Higher Order Logics (TPHOLs'98)}, volume
+ 1479 of {\em Lect.\ Notes in Comp.\ Sci.} Springer-Verlag, 1998.
\bibitem{Nipkow-CR}
Tobias Nipkow.
\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}).
-\newblock In Michael McRobbie and John~K. Slaney, editors, {\em Automated
- Deduction --- {CADE}-13 International Conference}, LNAI 1104, pages 733--747.
- Springer, 1996.
+\newblock In M.~McRobbie and J.K. Slaney, editors, {\em Automated Deduction ---
+ CADE-13}, volume 1104 of {\em Lect.\ Notes in Comp.\ Sci.}, pages 733--747.
+ Springer-Verlag, 1996.
\bibitem{nipkow-IMP}
Tobias Nipkow.
\newblock Winskel is (almost) right: Towards a mechanized semantics textbook.
-\newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software
- Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS},
- pages 180--192. Springer, 1996.
-
-\bibitem{nordstrom90}
-Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
-\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
-\newblock Oxford University Press, 1990.
+\newblock {\em Formal Aspects Comput.}, 10:171--186, 1998.
\bibitem{paulson85}
Lawrence~C. Paulson.
\newblock Verifying the unification algorithm in {LCF}.
\newblock {\em Science of Computer Programming}, 5:143--170, 1985.
-\bibitem{paulson87}
-Lawrence~C. Paulson.
-\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
-\newblock Cambridge University Press, 1987.
-
\bibitem{paulson-CADE}
Lawrence~C. Paulson.
\newblock A fixedpoint approach to implementing (co)inductive definitions.
@@ -131,30 +78,17 @@
\bibitem{paulson-set-II}
Lawrence~C. Paulson.
\newblock Set theory for verification: {II}. {Induction} and recursion.
-\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
-
-\bibitem{paulson-ns}
-Lawrence~C. Paulson.
-\newblock Mechanized proofs of security protocols: {Needham-Schroeder} with
- public keys.
-\newblock Technical Report 413, Computer Laboratory, University of Cambridge,
- January 1997.
+\newblock {\em J. Auto. Reas.}, 15(2):167--215, 1995.
\bibitem{paulson-coind}
Lawrence~C. Paulson.
\newblock Mechanizing coinduction and corecursion in higher-order logic.
-\newblock {\em Journal of Logic and Computation}, 7(2):175--204, March 1997.
+\newblock {\em J. Logic and Comput.}, 7(2):175--204, March 1997.
-\bibitem{paulson-security}
+\bibitem{paulson-jcs}
Lawrence~C. Paulson.
-\newblock Proving properties of security protocols by induction.
-\newblock In {\em 10th Computer Security Foundations Workshop}, pages 70--83.
- IEEE Computer Society Press, 1997.
-
-\bibitem{isabelle-ZF}
-Lawrence~C. Paulson.
-\newblock {Isabelle}'s logics: {FOL} and {ZF}.
-\newblock Technical report, Computer Laboratory, University of Cambridge, 1999.
+\newblock The inductive approach to verifying cryptographic protocols.
+\newblock {\em J. Comput. Secur.}, 6:85--128, 1998.
\bibitem{paulson-COLOG}
Lawrence~C. Paulson.
@@ -166,33 +100,20 @@
\bibitem{pelletier86}
F.~J. Pelletier.
\newblock Seventy-five problems for testing automatic theorem provers.
-\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
+\newblock {\em J. Auto. Reas.}, 2:191--216, 1986.
\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
\bibitem{plaisted90}
David~A. Plaisted.
\newblock A sequent-style model elimination strategy and a positive refinement.
-\newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990.
+\newblock {\em J. Auto. Reas.}, 6(4):389--402, 1990.
\bibitem{slind-tfl}
Konrad Slind.
-\newblock Function definition in higher-order logic.
-\newblock In von Wright et~al. \cite{tphols96}.
-
-\bibitem{takeuti87}
-G.~Takeuti.
-\newblock {\em Proof Theory}.
-\newblock North-Holland, 2nd edition, 1987.
-
-\bibitem{thompson91}
-Simon Thompson.
-\newblock {\em Type Theory and Functional Programming}.
-\newblock Addison-Wesley, 1991.
-
-\bibitem{tphols96}
-J.~von Wright, J.~Grundy, and J.~Harrison, editors.
-\newblock {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96}, LNCS
- 1125, 1996.
+\newblock Function definition in higher order logic.
+\newblock In J.~von Wright, J.~Grundy, and J.~Harrison, editors, {\em Theorem
+ Proving in Higher Order Logics}, volume 1125 of {\em Lect.\ Notes in Comp.\
+ Sci.}, pages 381--397. Springer-Verlag, 1996.
\bibitem{winskel93}
Glynn Winskel.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/manual.bib Wed May 05 16:44:42 1999 +0200
@@ -0,0 +1,937 @@
+% BibTeX database for the Isabelle documentation
+%
+% Lawrence C Paulson $Id$
+
+%publishers
+@string{AP="Academic Press"}
+@string{CUP="Cambridge University Press"}
+@string{IEEE="{\sc ieee} Computer Society Press"}
+@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
+@string{MIT="MIT Press"}
+@string{NH="North-Holland"}
+@string{Prentice="Prentice-Hall"}
+@string{Springer="Springer-Verlag"}
+
+%institutions
+@string{CUCL="Computer Laboratory, University of Cambridge"}
+
+%journals
+@string{FAC="Formal Aspects Comput."}
+@string{JAR="J. Auto. Reas."}
+@string{JCS="J. Comput. Secur."}
+@string{JFP="J. Func. Prog."}
+@string{JLC="J. Logic and Comput."}
+@string{JLP="J. Logic Prog."}
+@string{JSC="J. Symb. Comput."}
+@string{JSL="J. Symb. Logic"}
+@string{SIGPLAN="{SIGPLAN} Notices"}
+
+%conferences
+@string{CADE="International Conference on Automated Deduction"}
+@string{POPL="Symposium on Principles of Programming Languages"}
+@string{TYPES="Types for Proofs and Programs"}
+
+
+%A
+
+@incollection{abramsky90,
+ author = {Samson Abramsky},
+ title = {The Lazy Lambda Calculus},
+ pages = {65-116},
+ editor = {David A. Turner},
+ booktitle = {Research Topics in Functional Programming},
+ publisher = {Addison-Wesley},
+ year = 1990}
+
+@Unpublished{abrial93,
+ author = {J. R. Abrial and G. Laffitte},
+ title = {Towards the Mechanization of the Proofs of some Classical
+ Theorems of Set Theory},
+ note = {preprint},
+ year = 1993,
+ month = Feb}
+
+@incollection{aczel77,
+ author = {Peter Aczel},
+ title = {An Introduction to Inductive Definitions},
+ pages = {739-782},
+ crossref = {barwise-handbk}}
+
+@Book{aczel88,
+ author = {Peter Aczel},
+ title = {Non-Well-Founded Sets},
+ publisher = {CSLI},
+ year = 1988}
+
+@InProceedings{alf,
+ author = {Lena Magnusson and Bengt {Nordstr\"{o}m}},
+ title = {The {ALF} Proof Editor and Its Proof Engine},
+ crossref = {types93},
+ pages = {213-237}}
+
+@book{andrews86,
+ author = "Peter Andrews",
+ title = "An Introduction to Mathematical Logic and Type Theory: to Truth
+through Proof",
+ publisher = AP,
+ series = "Computer Science and Applied Mathematics",
+ year = 1986}
+
+%B
+
+@incollection{basin91,
+ author = {David Basin and Matt Kaufmann},
+ title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
+ Comparison},
+ crossref = {huet-plotkin91},
+ pages = {89-119}}
+
+@Article{boyer86,
+ author = {Robert Boyer and Ewing Lusk and William McCune and Ross
+ Overbeek and Mark Stickel and Lawrence Wos},
+ title = {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}
+ Axioms},
+ journal = JAR,
+ year = 1986,
+ volume = 2,
+ number = 3,
+ pages = {287-327}}
+
+@book{bm79,
+ author = {Robert S. Boyer and J Strother Moore},
+ title = {A Computational Logic},
+ publisher = {Academic Press},
+ year = 1979}
+
+@book{bm88book,
+ author = {Robert S. Boyer and J Strother Moore},
+ title = {A Computational Logic Handbook},
+ publisher = {Academic Press},
+ year = 1988}
+
+@Article{debruijn72,
+ author = {N. G. de Bruijn},
+ title = {Lambda Calculus Notation with Nameless Dummies,
+ a Tool for Automatic Formula Manipulation,
+ with Application to the {Church-Rosser Theorem}},
+ journal = {Indag. Math.},
+ volume = 34,
+ pages = {381-392},
+ year = 1972}
+
+%C
+
+@TechReport{camilleri92,
+ author = {J. Camilleri and T. F. Melham},
+ title = {Reasoning with Inductively Defined Relations in the
+ {HOL} Theorem Prover},
+ institution = CUCL,
+ year = 1992,
+ number = 265,
+ month = Aug}
+
+@Book{charniak80,
+ author = {E. Charniak and C. K. Riesbeck and D. V. McDermott},
+ title = {Artificial Intelligence Programming},
+ publisher = {Lawrence Erlbaum Associates},
+ year = 1980}
+
+@article{church40,
+ author = "Alonzo Church",
+ title = "A Formulation of the Simple Theory of Types",
+ journal = JSL,
+ year = 1940,
+ volume = 5,
+ pages = "56-68"}
+
+@PhdThesis{coen92,
+ author = {Martin D. Coen},
+ title = {Interactive Program Derivation},
+ school = {University of Cambridge},
+ note = {Computer Laboratory Technical Report 272},
+ month = nov,
+ year = 1992}
+
+@book{constable86,
+ author = {R. L. Constable and others},
+ title = {Implementing Mathematics with the Nuprl Proof
+ Development System},
+ publisher = Prentice,
+ year = 1986}
+
+%D
+
+@Book{davey&priestley,
+ author = {B. A. Davey and H. A. Priestley},
+ title = {Introduction to Lattices and Order},
+ publisher = CUP,
+ year = 1990}
+
+@Book{devlin79,
+ author = {Keith J. Devlin},
+ title = {Fundamentals of Contemporary Set Theory},
+ publisher = {Springer},
+ year = 1979}
+
+@book{dummett,
+ author = {Michael Dummett},
+ title = {Elements of Intuitionism},
+ year = 1977,
+ publisher = {Oxford University Press}}
+
+@incollection{dybjer91,
+ author = {Peter Dybjer},
+ title = {Inductive Sets and Families in {Martin-L\"of's} Type
+ Theory and Their Set-Theoretic Semantics},
+ crossref = {huet-plotkin91},
+ pages = {280-306}}
+
+@Article{dyckhoff,
+ author = {Roy Dyckhoff},
+ title = {Contraction-Free Sequent Calculi for Intuitionistic Logic},
+ journal = JSL,
+ year = 1992,
+ volume = 57,
+ number = 3,
+ pages = {795-807}}
+
+%F
+
+@InProceedings{felty91a,
+ Author = {Amy Felty},
+ Title = {A Logic Program for Transforming Sequent Proofs to Natural
+ Deduction Proofs},
+ crossref = {extensions91},
+ pages = {157-178}}
+
+@TechReport{frost93,
+ author = {Jacob Frost},
+ title = {A Case Study of Co-induction in {Isabelle HOL}},
+ institution = CUCL,
+ number = 308,
+ year = 1993,
+ month = Aug}
+
+%revised version of frost93
+@TechReport{frost95,
+ author = {Jacob Frost},
+ title = {A Case Study of Co-induction in {Isabelle}},
+ institution = CUCL,
+ number = 359,
+ year = 1995,
+ month = Feb}
+
+@inproceedings{OBJ,
+ author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
+ and J. Meseguer},
+ title = {Principles of {OBJ2}},
+ booktitle = POPL,
+ year = 1985,
+ pages = {52-66}}
+
+%G
+
+@book{gallier86,
+ author = {J. H. Gallier},
+ title = {Logic for Computer Science:
+ Foundations of Automatic Theorem Proving},
+ year = 1986,
+ publisher = {Harper \& Row}}
+
+@Book{galton90,
+ author = {Antony Galton},
+ title = {Logic for Information Technology},
+ publisher = {Wiley},
+ year = 1990}
+
+@InProceedings{gimenez-codifying,
+ author = {Eduardo Gim{\'e}nez},
+ title = {Codifying Guarded Definitions with Recursive Schemes},
+ crossref = {types94},
+ pages = {39-59}
+}
+
+@Book{mgordon-hol,
+ author = {M. J. C. Gordon and T. F. Melham},
+ title = {Introduction to {HOL}: A Theorem Proving Environment for
+ Higher Order Logic},
+ publisher = CUP,
+ year = 1993}
+
+@book{mgordon79,
+ author = {Michael J. C. Gordon and Robin Milner and Christopher P.
+ Wadsworth},
+ title = {Edinburgh {LCF}: A Mechanised Logic of Computation},
+ year = 1979,
+ publisher = {Springer},
+ series = {LNCS 78}}
+
+@InProceedings{gunter-trees,
+ author = {Elsa L. Gunter},
+ title = {A Broader Class of Trees for Recursive Type Definitions for
+ {HOL}},
+ crossref = {hug93},
+ pages = {141-154}}
+
+%H
+
+@Book{halmos60,
+ author = {Paul R. Halmos},
+ title = {Naive Set Theory},
+ publisher = {Van Nostrand},
+ year = 1960}
+
+@Book{hennessy90,
+ author = {Matthew Hennessy},
+ title = {The Semantics of Programming Languages: An Elementary
+ Introduction Using Structural Operational Semantics},
+ publisher = {Wiley},
+ year = 1990}
+
+@Article{haskell-report,
+ author = {Paul Hudak and Simon Peyton Jones and Philip Wadler},
+ title = {Report on the Programming Language {Haskell}: A
+ Non-strict, Purely Functional Language},
+ journal = SIGPLAN,
+ year = 1992,
+ volume = 27,
+ number = 5,
+ month = May,
+ note = {Version 1.2}}
+
+@Article{haskell-tutorial,
+ author = {Paul Hudak and Joseph H. Fasel},
+ title = {A Gentle Introduction to {Haskell}},
+ journal = SIGPLAN,
+ year = 1992,
+ volume = 27,
+ number = 5,
+ month = May}
+
+@article{huet75,
+ author = {G. P. Huet},
+ title = {A Unification Algorithm for Typed $\lambda$-Calculus},
+ journal = TCS,
+ volume = 1,
+ year = 1975,
+ pages = {27-57}}
+
+@article{huet78,
+ author = {G. P. Huet and B. Lang},
+ title = {Proving and Applying Program Transformations Expressed with
+ Second-Order Patterns},
+ journal = acta,
+ volume = 11,
+ year = 1978,
+ pages = {31-55}}
+
+@inproceedings{huet88,
+ author = {G\'erard Huet},
+ title = {Induction Principles Formalized in the {Calculus of
+ Constructions}},
+ booktitle = {Programming of Future Generation Computers},
+ editor = {K. Fuchi and M. Nivat},
+ year = 1988,
+ pages = {205-216},
+ publisher = {Elsevier}}
+
+%K
+
+@Book{kunen80,
+ author = {Kenneth Kunen},
+ title = {Set Theory: An Introduction to Independence Proofs},
+ publisher = NH,
+ year = 1980}
+
+%M
+
+@Article{mw81,
+ author = {Zohar Manna and Richard Waldinger},
+ title = {Deductive Synthesis of the Unification Algorithm},
+ journal = SCP,
+ year = 1981,
+ volume = 1,
+ number = 1,
+ pages = {5-48}}
+
+@InProceedings{martin-nipkow,
+ author = {Ursula Martin and Tobias Nipkow},
+ title = {Ordered Rewriting and Confluence},
+ crossref = {cade10},
+ pages = {366-380}}
+
+@book{martinlof84,
+ author = {Per Martin-L\"of},
+ title = {Intuitionistic type theory},
+ year = 1984,
+ publisher = {Bibliopolis}}
+
+@incollection{melham89,
+ author = {Thomas F. Melham},
+ title = {Automating Recursive Type Definitions in Higher Order
+ Logic},
+ pages = {341-386},
+ crossref = {birtwistle89}}
+
+@Article{miller-mixed,
+ Author = {Dale Miller},
+ Title = {Unification Under a Mixed Prefix},
+ journal = JSC,
+ volume = 14,
+ number = 4,
+ pages = {321-358},
+ Year = 1992}
+
+@Article{milner78,
+ author = {Robin Milner},
+ title = {A Theory of Type Polymorphism in Programming},
+ journal = "J. Comp.\ Sys.\ Sci.",
+ year = 1978,
+ volume = 17,
+ pages = {348-375}}
+
+@TechReport{milner-ind,
+ author = {Robin Milner},
+ title = {How to Derive Inductions in {LCF}},
+ institution = Edinburgh,
+ year = 1980,
+ type = {note}}
+
+@Article{milner-coind,
+ author = {Robin Milner and Mads Tofte},
+ title = {Co-induction in Relational Semantics},
+ journal = TCS,
+ year = 1991,
+ volume = 87,
+ pages = {209-220}}
+
+@Book{milner89,
+ author = {Robin Milner},
+ title = {Communication and Concurrency},
+ publisher = Prentice,
+ year = 1989}
+
+@PhdThesis{monahan84,
+ author = {Brian Q. Monahan},
+ title = {Data Type Proofs using Edinburgh {LCF}},
+ school = {University of Edinburgh},
+ year = 1984}
+
+%N
+
+@InProceedings{NaraschewskiW-TPHOLs98,
+ author = {Wolfgang Naraschewski and Markus Wenzel},
+ title =
+{Object-Oriented Verification based on Record Subtyping in Higher-Order Logic},
+ booktitle = {Theorem Proving in Higher Order Logics (TPHOLs'98)},
+ publisher = Springer,
+ volume = 1479,
+ series = LNCS,
+ year = 1998}
+
+@inproceedings{nazareth-nipkow,
+ author = {Dieter Nazareth and Tobias Nipkow},
+ title = {Formal Verification of Algorithm {W}: The Monomorphic Case},
+ crossref = {tphols96},
+ pages = {331-345},
+ year = 1996}
+
+@inproceedings{nipkow-W,
+ author = {Wolfgang Naraschewski and Tobias Nipkow},
+ title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
+ booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96},
+ editor = {E. Gim\'enez and C. Paulin-Mohring},
+ publisher = Springer,
+ series = LNCS,
+ volume = 1512,
+ pages = {317-332},
+ year = 1998}
+
+@inproceedings{Nipkow-CR,
+ author = {Tobias Nipkow},
+ title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
+ booktitle = {Automated Deduction --- CADE-13},
+ editor = {M. McRobbie and J.K. Slaney},
+ publisher = Springer,
+ series = LNCS,
+ volume = 1104,
+ pages = {733-747},
+ year = 1996}
+
+% WAS Nipkow-LICS-93
+@InProceedings{nipkow-patterns,
+ title = {Functional Unification of Higher-Order Patterns},
+ author = {Tobias Nipkow},
+ pages = {64-74},
+ crossref = {lics8},
+ url = {ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html},
+ keywords = {unification}}
+
+@article{nipkow-IMP,
+ author = {Tobias Nipkow},
+ title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
+ journal = FAC,
+ volume = 10,
+ pages = {171-186},
+ year = 1998}
+
+@article{nipkow-prehofer,
+ author = {Tobias Nipkow and Christian Prehofer},
+ title = {Type Reconstruction for Type Classes},
+ journal = JFP,
+ volume = 5,
+ number = 2,
+ year = 1995,
+ pages = {201-224}}
+
+@Article{noel,
+ author = {Philippe No{\"e}l},
+ title = {Experimenting with {Isabelle} in {ZF} Set Theory},
+ journal = JAR,
+ volume = 10,
+ number = 1,
+ pages = {15-58},
+ year = 1993}
+
+@book{nordstrom90,
+ author = {Bengt {Nordstr\"om} and Kent Petersson and Jan Smith},
+ title = {Programming in {Martin-L\"of}'s Type Theory. An
+ Introduction},
+ publisher = {Oxford University Press},
+ year = 1990}
+
+%O
+
+@Manual{pvs-language,
+ title = {The {PVS} specification language},
+ author = {S. Owre and N. Shankar and J. M. Rushby},
+ organization = {Computer Science Laboratory, SRI International},
+ address = {Menlo Park, CA},
+ note = {Beta release},
+ year = 1993,
+ month = apr,
+ url = {\verb|http://www.csl.sri.com/reports/pvs-language.dvi.Z|}}
+
+%P
+
+% replaces paulin92
+@InProceedings{paulin-tlca,
+ author = {Christine Paulin-Mohring},
+ title = {Inductive Definitions in the System {Coq}: Rules and
+ Properties},
+ crossref = {tlca93},
+ pages = {328-345}}
+
+@InProceedings{paulson-CADE,
+ author = {Lawrence C. Paulson},
+ title = {A Fixedpoint Approach to Implementing (Co)Inductive
+ Definitions},
+ pages = {148-161},
+ crossref = {cade12}}
+
+@InProceedings{paulson-COLOG,
+ author = {Lawrence C. Paulson},
+ title = {A Formulation of the Simple Theory of Types (for
+ {Isabelle})},
+ pages = {246-274},
+ crossref = {colog88},
+ url = {http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}
+
+@Article{paulson-coind,
+ author = {Lawrence C. Paulson},
+ title = {Mechanizing Coinduction and Corecursion in Higher-Order
+ Logic},
+ journal = JLC,
+ year = 1997,
+ volume = 7,
+ number = 2,
+ month = mar,
+ pages = {175-204}}
+
+@techreport{isabelle-ZF,
+ author = {Lawrence C. Paulson},
+ title = {{Isabelle}'s Logics: {FOL} and {ZF}},
+ institution = CUCL,
+ year = 1999}
+
+@article{paulson-found,
+ author = {Lawrence C. Paulson},
+ title = {The Foundation of a Generic Theorem Prover},
+ journal = JAR,
+ volume = 5,
+ number = 3,
+ pages = {363-397},
+ year = 1989,
+ url = {http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}
+
+%replaces paulson-final
+@Article{paulson-mscs,
+ author = {Lawrence C. Paulson},
+ title = {Final Coalgebras as Greatest Fixed Points in ZF Set Theory},
+ journal = {Mathematical Structures in Computer Science},
+ year = 1999,
+ volume = 9,
+ note = {in press}}
+
+@InCollection{paulson-generic,
+ author = {Lawrence C. Paulson},
+ title = {Generic Automatic Proof Tools},
+ crossref = {wos-fest},
+ chapter = 3}
+
+@Article{paulson-gr,
+ author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
+ title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of
+ Choice},
+ journal = JAR,
+ year = 1996,
+ volume = 17,
+ number = 3,
+ month = dec,
+ pages = {291-323}}
+
+@InCollection{paulson-handbook,
+ author = {Lawrence C. Paulson},
+ title = {Designing a Theorem Prover},
+ crossref = {handbk-lics2},
+ pages = {415-475}}
+
+@Book{paulson-isa-book,
+ author = {Lawrence C. Paulson},
+ title = {Isabelle: A Generic Theorem Prover},
+ publisher = {Springer},
+ year = 1994,
+ note = {LNCS 828}}
+
+@InCollection{paulson-markt,
+ author = {Lawrence C. Paulson},
+ title = {Tool Support for Logics of Programs},
+ booktitle = {Mathematical Methods in Program Development:
+ Summer School Marktoberdorf 1996},
+ publisher = {Springer},
+ pages = {461-498},
+ year = {Published 1997},
+ editor = {Manfred Broy},
+ series = {NATO ASI Series F}}
+
+%replaces Paulson-ML and paulson91
+@book{paulson-ml2,
+ author = {Lawrence C. Paulson},
+ title = {{ML} for the Working Programmer},
+ year = 1996,
+ edition = {2nd},
+ publisher = CUP}
+
+@article{paulson-natural,
+ author = {Lawrence C. Paulson},
+ title = {Natural Deduction as Higher-order Resolution},
+ journal = JLP,
+ volume = 3,
+ pages = {237-258},
+ year = 1986,
+ url = {http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}
+
+@Article{paulson-set-I,
+ author = {Lawrence C. Paulson},
+ title = {Set Theory for Verification: {I}. {From}
+ Foundations to Functions},
+ journal = JAR,
+ volume = 11,
+ number = 3,
+ pages = {353-389},
+ year = 1993,
+ url = {ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}
+
+@Article{paulson-set-II,
+ author = {Lawrence C. Paulson},
+ title = {Set Theory for Verification: {II}. {Induction} and
+ Recursion},
+ journal = JAR,
+ volume = 15,
+ number = 2,
+ pages = {167-215},
+ year = 1995,
+ url = {http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}
+
+@article{paulson85,
+ author = {Lawrence C. Paulson},
+ title = {Verifying the Unification Algorithm in {LCF}},
+ journal = SCP,
+ volume = 5,
+ pages = {143-170},
+ year = 1985}
+
+%replqces Paulson-LCF
+@book{paulson87,
+ author = {Lawrence C. Paulson},
+ title = {Logic and Computation: Interactive proof with Cambridge
+ LCF},
+ year = 1987,
+ publisher = CUP}
+
+@incollection{paulson700,
+ author = {Lawrence C. Paulson},
+ title = {{Isabelle}: The Next 700 Theorem Provers},
+ crossref = {odifreddi90},
+ pages = {361-386},
+ url = {http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}
+
+% replaces paulson-ns and paulson-security
+@Article{paulson-jcs,
+ author = {Lawrence C. Paulson},
+ title = {The Inductive Approach to Verifying Cryptographic Protocols},
+ journal = JCS,
+ year = 1998,
+ volume = 6,
+ pages = {85-128}}
+
+@article{pelletier86,
+ author = {F. J. Pelletier},
+ title = {Seventy-five Problems for Testing Automatic Theorem
+ Provers},
+ journal = JAR,
+ volume = 2,
+ pages = {191-216},
+ year = 1986,
+ note = {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}}
+
+@Article{pitts94,
+ author = {Andrew M. Pitts},
+ title = {A Co-induction Principle for Recursively Defined Domains},
+ journal = TCS,
+ volume = 124,
+ pages = {195-219},
+ year = 1994}
+
+@Article{plaisted90,
+ author = {David A. Plaisted},
+ title = {A Sequent-Style Model Elimination Strategy and a Positive
+ Refinement},
+ journal = JAR,
+ year = 1990,
+ volume = 6,
+ number = 4,
+ pages = {389-402}}
+
+%Q
+
+@Article{quaife92,
+ author = {Art Quaife},
+ title = {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set
+ Theory},
+ journal = JAR,
+ year = 1992,
+ volume = 8,
+ number = 1,
+ pages = {91-147}}
+
+%R
+
+@TechReport{rasmussen95,
+ author = {Ole Rasmussen},
+ title = {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting
+ Experiment},
+ institution = {Computer Laboratory, University of Cambridge},
+ year = 1995,
+ number = 364,
+ month = may,
+ url = {http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}
+
+@Book{reeves90,
+ author = {Steve Reeves and Michael Clarke},
+ title = {Logic for Computer Science},
+ publisher = {Addison-Wesley},
+ year = 1990}
+
+%S
+
+@inproceedings{saaltink-fme,
+ author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
+ Dan Craigen and Irwin Meisels},
+ title = {An {EVES} Data Abstraction Example},
+ pages = {578-596},
+ crossref = {fme93}}
+
+@inproceedings{slind-tfl,
+ author = {Konrad Slind},
+ title = {Function Definition in Higher Order Logic},
+ booktitle = {Theorem Proving in Higher Order Logics},
+ editor = {J. von Wright and J. Grundy and J. Harrison},
+ publisher = Springer,
+ series = LNCS,
+ volume = 1125,
+ pages = {381-397},
+ year = 1996}
+
+@book{suppes72,
+ author = {Patrick Suppes},
+ title = {Axiomatic Set Theory},
+ year = 1972,
+ publisher = {Dover}}
+
+@InCollection{szasz93,
+ author = {Nora Szasz},
+ title = {A Machine Checked Proof that {Ackermann's} Function is not
+ Primitive Recursive},
+ crossref = {huet-plotkin93},
+ pages = {317-338}}
+
+%T
+
+@book{takeuti87,
+ author = {G. Takeuti},
+ title = {Proof Theory},
+ year = 1987,
+ publisher = NH,
+ edition = {2nd}}
+
+@Book{thompson91,
+ author = {Simon Thompson},
+ title = {Type Theory and Functional Programming},
+ publisher = {Addison-Wesley},
+ year = 1991}
+
+%V
+
+@Unpublished{voelker94,
+ author = {Norbert V\"olker},
+ title = {The Verification of a Timer Program using {Isabelle/HOL}},
+ url = {ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz},
+ year = 1994,
+ month = aug}
+
+%W
+
+@book{principia,
+ author = {A. N. Whitehead and B. Russell},
+ title = {Principia Mathematica},
+ year = 1962,
+ publisher = CUP,
+ note = {Paperback edition to *56,
+ abridged from the 2nd edition (1927)}}
+
+@book{winskel93,
+ author = {Glynn Winskel},
+ title = {The Formal Semantics of Programming Languages},
+ publisher = MIT,year=1993}
+
+@InCollection{wos-bledsoe,
+ author = {Larry Wos},
+ title = {Automated Reasoning and {Bledsoe's} Dream for the Field},
+ crossref = {bledsoe-fest},
+ pages = {297-342}}
+
+
+% CROSS REFERENCES
+
+@book{handbk-lics2,
+ editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
+ title = {Handbook of Logic in Computer Science},
+ booktitle = {Handbook of Logic in Computer Science},
+ publisher = {Oxford University Press},
+ year = 1992,
+ volume = 2}
+
+@book{types93,
+ editor = {Henk Barendregt and Tobias Nipkow},
+ title = TYPES # {: International Workshop {TYPES '93}},
+ booktitle = TYPES # {: International Workshop {TYPES '93}},
+ year = {published 1994},
+ publisher = {Springer},
+ series = {LNCS 806}}
+
+@Proceedings{tlca93,
+ title = {Typed Lambda Calculi and Applications},
+ booktitle = {Typed Lambda Calculi and Applications},
+ editor = {M. Bezem and J.F. Groote},
+ year = 1993,
+ publisher = {Springer},
+ series = {LNCS 664}}
+
+@book{bledsoe-fest,
+ title = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
+ booktitle = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
+ publisher = {Kluwer Academic Publishers},
+ year = 1991,
+ editor = {Robert S. Boyer}}
+
+@Proceedings{cade12,
+ editor = {Alan Bundy},
+ title = {Automated Deduction --- {CADE}-12
+ International Conference},
+ booktitle = {Automated Deduction --- {CADE}-12
+ International Conference},
+ year = 1994,
+ series = {LNAI 814},
+ publisher = {Springer}}
+
+@book{types94,
+ editor = {Peter Dybjer and Bengt Nordstr{\"om} and Jan Smith},
+ title = TYPES # {: International Workshop {TYPES '94}},
+ booktitle = TYPES # {: International Workshop {TYPES '94}},
+ year = 1995,
+ publisher = {Springer},
+ series = {LNCS 996}}
+
+@book{huet-plotkin91,
+ editor = {{G\'erard} Huet and Gordon Plotkin},
+ title = {Logical Frameworks},
+ booktitle = {Logical Frameworks},
+ publisher = CUP,
+ year = 1991}
+
+@proceedings{colog88,
+ editor = {P. Martin-L\"of and G. Mints},
+ title = {COLOG-88: International Conference on Computer Logic},
+ booktitle = {COLOG-88: International Conference on Computer Logic},
+ year = {Published 1990},
+ publisher = {Springer},
+ organization = {Estonian Academy of Sciences},
+ address = {Tallinn},
+ series = {LNCS 417}}
+
+@book{odifreddi90,
+ editor = {P. Odifreddi},
+ title = {Logic and Computer Science},
+ booktitle = {Logic and Computer Science},
+ publisher = {Academic Press},
+ year = 1990}
+
+@proceedings{extensions91,
+ editor = {Peter Schroeder-Heister},
+ title = {Extensions of Logic Programming},
+ booktitle = {Extensions of Logic Programming},
+ year = 1991,
+ series = {LNAI 475},
+ publisher = {Springer}}
+
+@proceedings{cade10,
+ editor = {Mark E. Stickel},
+ title = {10th } # CADE,
+ booktitle = {10th } # CADE,
+ year = 1990,
+ publisher = {Springer},
+ series = {LNAI 449}}
+
+@Proceedings{lics8,
+ editor = {M. Vardi},
+ title = {Eighth Annual Symposium on Logic in Computer Science},
+ booktitle = {Eighth Annual Symposium on Logic in Computer Science},
+ publisher = IEEE,
+ year = 1993}
+
+@book{wos-fest,
+ title = {Automated Reasoning and its Applications:
+ Essays in Honor of {Larry Wos}},
+ booktitle = {Automated Reasoning and its Applications:
+ Essays in Honor of {Larry Wos}},
+ publisher = {MIT Press},
+ year = 1997,
+ editor = {Robert Veroff}}
+
+@Proceedings{tphols96,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
+ editor = {J. von Wright and J. Grundy and J. Harrison},
+ series = {LNCS 1125},
+ year = 1996}