Now uses manual.bib; some references updated
authorpaulson
Wed May 05 16:44:42 1999 +0200 (1999-05-05)
changeset 6592c120262044b6
parent 6591 6a753a6d6738
child 6593 62204772812f
Now uses manual.bib; some references updated
doc-src/HOL/HOL.tex
doc-src/HOL/logics-HOL.bbl
doc-src/HOL/logics-HOL.tex
doc-src/Intro/foundations.tex
doc-src/Intro/intro.bbl
doc-src/Intro/intro.tex
doc-src/Logics/logics.bbl
doc-src/Logics/logics.tex
doc-src/Ref/classical.tex
doc-src/Ref/defining.tex
doc-src/Ref/ref.bbl
doc-src/Ref/ref.tex
doc-src/Ref/theories.tex
doc-src/ZF/ZF.tex
doc-src/ZF/logics-ZF.bbl
doc-src/ZF/logics-ZF.tex
doc-src/isabelle.bib
doc-src/manual.bib
     1.1 --- a/doc-src/HOL/HOL.tex	Wed May 05 14:31:31 1999 +0200
     1.2 +++ b/doc-src/HOL/HOL.tex	Wed May 05 16:44:42 1999 +0200
     1.3 @@ -1547,7 +1547,7 @@
     1.4  slightly more advanced, though, supporting \emph{extensible record schemes}.
     1.5  This admits operations that are polymorphic with respect to record extension,
     1.6  yielding ``object-oriented'' effects like (single) inheritance.  See also
     1.7 -\cite{Naraschewski-Wenzel:1998:TPHOL} for more details on object-oriented
     1.8 +\cite{NaraschewskiW-TPHOLs98} for more details on object-oriented
     1.9  verification and record subtyping in HOL.
    1.10  
    1.11  
    1.12 @@ -2763,12 +2763,12 @@
    1.13  
    1.14  \section{The examples directories}
    1.15  
    1.16 -Directory \texttt{HOL/Auth} contains theories for proving the correctness of 
    1.17 -cryptographic protocols.  The approach is based upon operational 
    1.18 -semantics~\cite{paulson-security} rather than the more usual belief logics.
    1.19 -On the same directory are proofs for some standard examples, such as the 
    1.20 -Needham-Schroeder public-key authentication protocol~\cite{paulson-ns} 
    1.21 -and the Otway-Rees protocol.
    1.22 +Directory \texttt{HOL/Auth} contains theories for proving the correctness of
    1.23 +cryptographic protocols~\cite{paulson-jcs}.  The approach is based upon
    1.24 +operational semantics rather than the more usual belief logics.  On the same
    1.25 +directory are proofs for some standard examples, such as the Needham-Schroeder
    1.26 +public-key authentication protocol and the Otway-Rees
    1.27 +protocol.
    1.28  
    1.29  Directory \texttt{HOL/IMP} contains a formalization of various denotational,
    1.30  operational and axiomatic semantics of a simple while-language, the necessary
     2.1 --- a/doc-src/HOL/logics-HOL.bbl	Wed May 05 14:31:31 1999 +0200
     2.2 +++ b/doc-src/HOL/logics-HOL.bbl	Wed May 05 16:44:42 1999 +0200
     2.3 @@ -1,34 +1,15 @@
     2.4  \begin{thebibliography}{10}
     2.5  
     2.6  \bibitem{andrews86}
     2.7 -Peter~B. Andrews.
     2.8 -\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
     2.9 -  Through Proof}.
    2.10 -\newblock Academic Press, 1986.
    2.11 +Peter Andrews.
    2.12 +\newblock {\em An Introduction to Mathematical Logic and Type Theory: to Truth
    2.13 +  through Proof}.
    2.14 +\newblock Computer Science and Applied Mathematics. Academic Press, 1986.
    2.15  
    2.16  \bibitem{church40}
    2.17  Alonzo Church.
    2.18  \newblock A formulation of the simple theory of types.
    2.19 -\newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.
    2.20 -
    2.21 -\bibitem{coen92}
    2.22 -Martin~D. Coen.
    2.23 -\newblock {\em Interactive Program Derivation}.
    2.24 -\newblock PhD thesis, University of Cambridge, November 1992.
    2.25 -\newblock Computer Laboratory Technical Report 272.
    2.26 -
    2.27 -\bibitem{constable86}
    2.28 -R.~L. Constable et~al.
    2.29 -\newblock {\em Implementing Mathematics with the Nuprl Proof Development
    2.30 -  System}.
    2.31 -\newblock Prentice-Hall, 1986.
    2.32 -
    2.33 -\bibitem{felty91a}
    2.34 -Amy Felty.
    2.35 -\newblock A logic program for transforming sequent proofs to natural deduction
    2.36 -  proofs.
    2.37 -\newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic
    2.38 -  Programming}, LNAI 475, pages 157--178. Springer, 1991.
    2.39 +\newblock {\em J. Symb. Logic}, 5:56--68, 1940.
    2.40  
    2.41  \bibitem{frost93}
    2.42  Jacob Frost.
    2.43 @@ -36,92 +17,58 @@
    2.44  \newblock Technical Report 308, Computer Laboratory, University of Cambridge,
    2.45    August 1993.
    2.46  
    2.47 -\bibitem{gallier86}
    2.48 -J.~H. Gallier.
    2.49 -\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
    2.50 -  Proving}.
    2.51 -\newblock Harper \& Row, 1986.
    2.52 -
    2.53  \bibitem{mgordon-hol}
    2.54  M.~J.~C. Gordon and T.~F. Melham.
    2.55  \newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
    2.56    Order Logic}.
    2.57  \newblock Cambridge University Press, 1993.
    2.58  
    2.59 -\bibitem{huet78}
    2.60 -G.~P. Huet and B.~Lang.
    2.61 -\newblock Proving and applying program transformations expressed with
    2.62 -  second-order patterns.
    2.63 -\newblock {\em Acta Informatica}, 11:31--55, 1978.
    2.64 -
    2.65 -\bibitem{alf}
    2.66 -Lena Magnusson and Bengt {Nordstr\"{o}m}.
    2.67 -\newblock The {ALF} proof editor and its proof engine.
    2.68 -\newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs
    2.69 -  and Programs: International Workshop {TYPES '93}}, LNCS 806, pages 213--237.
    2.70 -  Springer, published 1994.
    2.71 -
    2.72  \bibitem{mw81}
    2.73  Zohar Manna and Richard Waldinger.
    2.74  \newblock Deductive synthesis of the unification algorithm.
    2.75  \newblock {\em Science of Computer Programming}, 1(1):5--48, 1981.
    2.76  
    2.77 -\bibitem{martinlof84}
    2.78 -Per Martin-L\"of.
    2.79 -\newblock {\em Intuitionistic type theory}.
    2.80 -\newblock Bibliopolis, 1984.
    2.81 -
    2.82  \bibitem{milner78}
    2.83  Robin Milner.
    2.84  \newblock A theory of type polymorphism in programming.
    2.85 -\newblock {\em Journal of Computer and System Sciences}, 17:348--375, 1978.
    2.86 +\newblock {\em J. Comp.\ Sys.\ Sci.}, 17:348--375, 1978.
    2.87  
    2.88  \bibitem{milner-coind}
    2.89  Robin Milner and Mads Tofte.
    2.90  \newblock Co-induction in relational semantics.
    2.91  \newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
    2.92  
    2.93 -\bibitem{Naraschewski-Wenzel:1998:TPHOL}
    2.94 +\bibitem{nipkow-W}
    2.95 +Wolfgang Naraschewski and Tobias Nipkow.
    2.96 +\newblock Type inference verified: Algorithm {W} in {Isabelle/HOL}.
    2.97 +\newblock In E.~Gim\'enez and C.~Paulin-Mohring, editors, {\em Types for Proofs
    2.98 +  and Programs: Intl. Workshop TYPES '96}, volume 1512 of {\em Lect.\ Notes in
    2.99 +  Comp.\ Sci.}, pages 317--332. Springer-Verlag, 1998.
   2.100 +
   2.101 +\bibitem{NaraschewskiW-TPHOLs98}
   2.102  Wolfgang Naraschewski and Markus Wenzel.
   2.103  \newblock Object-oriented verification based on record subtyping in
   2.104    higher-order logic.
   2.105 -\newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in
   2.106 -  Higher Order Logics: {TPHOLs} '98}, LNCS 1479, pages 349--366, 1998.
   2.107 -
   2.108 -\bibitem{nazareth-nipkow}
   2.109 -Dieter Nazareth and Tobias Nipkow.
   2.110 -\newblock Formal verification of algorithm {W}: The monomorphic case.
   2.111 -\newblock In von Wright et~al. \cite{tphols96}, pages 331--345.
   2.112 +\newblock In {\em Theorem Proving in Higher Order Logics (TPHOLs'98)}, volume
   2.113 +  1479 of {\em Lect.\ Notes in Comp.\ Sci.} Springer-Verlag, 1998.
   2.114  
   2.115  \bibitem{Nipkow-CR}
   2.116  Tobias Nipkow.
   2.117  \newblock More {Church-Rosser} proofs (in {Isabelle/HOL}).
   2.118 -\newblock In Michael McRobbie and John~K. Slaney, editors, {\em Automated
   2.119 -  Deduction --- {CADE}-13 International Conference}, LNAI 1104, pages 733--747.
   2.120 -  Springer, 1996.
   2.121 +\newblock In M.~McRobbie and J.K. Slaney, editors, {\em Automated Deduction ---
   2.122 +  CADE-13}, volume 1104 of {\em Lect.\ Notes in Comp.\ Sci.}, pages 733--747.
   2.123 +  Springer-Verlag, 1996.
   2.124  
   2.125  \bibitem{nipkow-IMP}
   2.126  Tobias Nipkow.
   2.127  \newblock Winskel is (almost) right: Towards a mechanized semantics textbook.
   2.128 -\newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software
   2.129 -  Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS},
   2.130 -  pages 180--192. Springer, 1996.
   2.131 -
   2.132 -\bibitem{nordstrom90}
   2.133 -Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
   2.134 -\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
   2.135 -\newblock Oxford University Press, 1990.
   2.136 +\newblock {\em Formal Aspects Comput.}, 10:171--186, 1998.
   2.137  
   2.138  \bibitem{paulson85}
   2.139  Lawrence~C. Paulson.
   2.140  \newblock Verifying the unification algorithm in {LCF}.
   2.141  \newblock {\em Science of Computer Programming}, 5:143--170, 1985.
   2.142  
   2.143 -\bibitem{paulson87}
   2.144 -Lawrence~C. Paulson.
   2.145 -\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
   2.146 -\newblock Cambridge University Press, 1987.
   2.147 -
   2.148  \bibitem{paulson-CADE}
   2.149  Lawrence~C. Paulson.
   2.150  \newblock A fixedpoint approach to implementing (co)inductive definitions.
   2.151 @@ -131,30 +78,17 @@
   2.152  \bibitem{paulson-set-II}
   2.153  Lawrence~C. Paulson.
   2.154  \newblock Set theory for verification: {II}. {Induction} and recursion.
   2.155 -\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
   2.156 -
   2.157 -\bibitem{paulson-ns}
   2.158 -Lawrence~C. Paulson.
   2.159 -\newblock Mechanized proofs of security protocols: {Needham-Schroeder} with
   2.160 -  public keys.
   2.161 -\newblock Technical Report 413, Computer Laboratory, University of Cambridge,
   2.162 -  January 1997.
   2.163 +\newblock {\em J. Auto. Reas.}, 15(2):167--215, 1995.
   2.164  
   2.165  \bibitem{paulson-coind}
   2.166  Lawrence~C. Paulson.
   2.167  \newblock Mechanizing coinduction and corecursion in higher-order logic.
   2.168 -\newblock {\em Journal of Logic and Computation}, 7(2):175--204, March 1997.
   2.169 +\newblock {\em J. Logic and Comput.}, 7(2):175--204, March 1997.
   2.170  
   2.171 -\bibitem{paulson-security}
   2.172 +\bibitem{paulson-jcs}
   2.173  Lawrence~C. Paulson.
   2.174 -\newblock Proving properties of security protocols by induction.
   2.175 -\newblock In {\em 10th Computer Security Foundations Workshop}, pages 70--83.
   2.176 -  IEEE Computer Society Press, 1997.
   2.177 -
   2.178 -\bibitem{isabelle-ZF}
   2.179 -Lawrence~C. Paulson.
   2.180 -\newblock {Isabelle}'s logics: {FOL} and {ZF}.
   2.181 -\newblock Technical report, Computer Laboratory, University of Cambridge, 1999.
   2.182 +\newblock The inductive approach to verifying cryptographic protocols.
   2.183 +\newblock {\em J. Comput. Secur.}, 6:85--128, 1998.
   2.184  
   2.185  \bibitem{paulson-COLOG}
   2.186  Lawrence~C. Paulson.
   2.187 @@ -166,33 +100,20 @@
   2.188  \bibitem{pelletier86}
   2.189  F.~J. Pelletier.
   2.190  \newblock Seventy-five problems for testing automatic theorem provers.
   2.191 -\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
   2.192 +\newblock {\em J. Auto. Reas.}, 2:191--216, 1986.
   2.193  \newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
   2.194  
   2.195  \bibitem{plaisted90}
   2.196  David~A. Plaisted.
   2.197  \newblock A sequent-style model elimination strategy and a positive refinement.
   2.198 -\newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990.
   2.199 +\newblock {\em J. Auto. Reas.}, 6(4):389--402, 1990.
   2.200  
   2.201  \bibitem{slind-tfl}
   2.202  Konrad Slind.
   2.203 -\newblock Function definition in higher-order logic.
   2.204 -\newblock In von Wright et~al. \cite{tphols96}.
   2.205 -
   2.206 -\bibitem{takeuti87}
   2.207 -G.~Takeuti.
   2.208 -\newblock {\em Proof Theory}.
   2.209 -\newblock North-Holland, 2nd edition, 1987.
   2.210 -
   2.211 -\bibitem{thompson91}
   2.212 -Simon Thompson.
   2.213 -\newblock {\em Type Theory and Functional Programming}.
   2.214 -\newblock Addison-Wesley, 1991.
   2.215 -
   2.216 -\bibitem{tphols96}
   2.217 -J.~von Wright, J.~Grundy, and J.~Harrison, editors.
   2.218 -\newblock {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96}, LNCS
   2.219 -  1125, 1996.
   2.220 +\newblock Function definition in higher order logic.
   2.221 +\newblock In J.~von Wright, J.~Grundy, and J.~Harrison, editors, {\em Theorem
   2.222 +  Proving in Higher Order Logics}, volume 1125 of {\em Lect.\ Notes in Comp.\
   2.223 +  Sci.}, pages 381--397. Springer-Verlag, 1996.
   2.224  
   2.225  \bibitem{winskel93}
   2.226  Glynn Winskel.
     3.1 --- a/doc-src/HOL/logics-HOL.tex	Wed May 05 14:31:31 1999 +0200
     3.2 +++ b/doc-src/HOL/logics-HOL.tex	Wed May 05 16:44:42 1999 +0200
     3.3 @@ -56,7 +56,6 @@
     3.4  \include{../Logics/syntax}
     3.5  \include{HOL}
     3.6  \bibliographystyle{plain}
     3.7 -\bibliography{../isabelle}
     3.8 -%\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref}
     3.9 +\bibliography{../manual}
    3.10  \input{logics-HOL.ind}
    3.11  \end{document}
     4.1 --- a/doc-src/Intro/foundations.tex	Wed May 05 14:31:31 1999 +0200
     4.2 +++ b/doc-src/Intro/foundations.tex	Wed May 05 16:44:42 1999 +0200
     4.3 @@ -959,7 +959,7 @@
     4.4  rather than on individual subgoals.  An Isabelle tactic is a function that
     4.5  takes a proof state and returns a sequence (lazy list) of possible
     4.6  successor states.  Lazy lists are coded in ML as functions, a standard
     4.7 -technique~\cite{paulson91}.  Isabelle represents proof states by theorems.
     4.8 +technique~\cite{paulson-ml2}.  Isabelle represents proof states by theorems.
     4.9  
    4.10  Basic tactics execute the meta-rules described above, operating on a
    4.11  given subgoal.  The {\bf resolution tactics} take a list of rules and
     5.1 --- a/doc-src/Intro/intro.bbl	Wed May 05 14:31:31 1999 +0200
     5.2 +++ b/doc-src/Intro/intro.bbl	Wed May 05 16:44:42 1999 +0200
     5.3 @@ -69,11 +69,6 @@
     5.4  \newblock In P.~Odifreddi, editor, {\em Logic and Computer Science}, pages
     5.5    361--386. Academic Press, 1990.
     5.6  
     5.7 -\bibitem{paulson91}
     5.8 -Lawrence~C. Paulson.
     5.9 -\newblock {\em {ML} for the Working Programmer}.
    5.10 -\newblock Cambridge University Press, 1991.
    5.11 -
    5.12  \bibitem{paulson-handbook}
    5.13  Lawrence~C. Paulson.
    5.14  \newblock Designing a theorem prover.
    5.15 @@ -81,6 +76,11 @@
    5.16    Handbook of Logic in Computer Science}, volume~2, pages 415--475. Oxford
    5.17    University Press, 1992.
    5.18  
    5.19 +\bibitem{paulson-ml2}
    5.20 +Lawrence~C. Paulson.
    5.21 +\newblock {\em {ML} for the Working Programmer}.
    5.22 +\newblock Cambridge University Press, 2nd edition, 1996.
    5.23 +
    5.24  \bibitem{pelletier86}
    5.25  F.~J. Pelletier.
    5.26  \newblock Seventy-five problems for testing automatic theorem provers.
     6.1 --- a/doc-src/Intro/intro.tex	Wed May 05 14:31:31 1999 +0200
     6.2 +++ b/doc-src/Intro/intro.tex	Wed May 05 16:44:42 1999 +0200
     6.3 @@ -64,7 +64,7 @@
     6.4  knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user
     6.5  interface.  Advanced Isabelle theorem proving can involve writing \ML{}
     6.6  code, possibly with Isabelle's sources at hand.  My book
     6.7 -on~\ML{}~\cite{paulson91} covers much material connected with Isabelle,
     6.8 +on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle,
     6.9  including a simple theorem prover.  Users must be familiar with logic as
    6.10  used in computer science; there are many good
    6.11  texts~\cite{galton90,reeves90}.
    6.12 @@ -135,7 +135,7 @@
    6.13  \include{advanced}
    6.14  
    6.15  \bibliographystyle{plain} \small\raggedright\frenchspacing
    6.16 -\bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref}
    6.17 +\bibliography{../manual}
    6.18  
    6.19  \input{intro.ind}
    6.20  \end{document}
     7.1 --- a/doc-src/Logics/logics.bbl	Wed May 05 14:31:31 1999 +0200
     7.2 +++ b/doc-src/Logics/logics.bbl	Wed May 05 16:44:42 1999 +0200
     7.3 @@ -1,16 +1,5 @@
     7.4  \begin{thebibliography}{10}
     7.5  
     7.6 -\bibitem{andrews86}
     7.7 -Peter~B. Andrews.
     7.8 -\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
     7.9 -  Through Proof}.
    7.10 -\newblock Academic Press, 1986.
    7.11 -
    7.12 -\bibitem{church40}
    7.13 -Alonzo Church.
    7.14 -\newblock A formulation of the simple theory of types.
    7.15 -\newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.
    7.16 -
    7.17  \bibitem{coen92}
    7.18  Martin~D. Coen.
    7.19  \newblock {\em Interactive Program Derivation}.
    7.20 @@ -30,24 +19,12 @@
    7.21  \newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic
    7.22    Programming}, LNAI 475, pages 157--178. Springer, 1991.
    7.23  
    7.24 -\bibitem{frost93}
    7.25 -Jacob Frost.
    7.26 -\newblock A case study of co-induction in {Isabelle HOL}.
    7.27 -\newblock Technical Report 308, Computer Laboratory, University of Cambridge,
    7.28 -  August 1993.
    7.29 -
    7.30  \bibitem{gallier86}
    7.31  J.~H. Gallier.
    7.32  \newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
    7.33    Proving}.
    7.34  \newblock Harper \& Row, 1986.
    7.35  
    7.36 -\bibitem{mgordon-hol}
    7.37 -M.~J.~C. Gordon and T.~F. Melham.
    7.38 -\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
    7.39 -  Order Logic}.
    7.40 -\newblock Cambridge University Press, 1993.
    7.41 -
    7.42  \bibitem{huet78}
    7.43  G.~P. Huet and B.~Lang.
    7.44  \newblock Proving and applying program transformations expressed with
    7.45 @@ -61,124 +38,32 @@
    7.46    and Programs: International Workshop {TYPES '93}}, LNCS 806, pages 213--237.
    7.47    Springer, published 1994.
    7.48  
    7.49 -\bibitem{mw81}
    7.50 -Zohar Manna and Richard Waldinger.
    7.51 -\newblock Deductive synthesis of the unification algorithm.
    7.52 -\newblock {\em Science of Computer Programming}, 1(1):5--48, 1981.
    7.53 -
    7.54  \bibitem{martinlof84}
    7.55  Per Martin-L\"of.
    7.56  \newblock {\em Intuitionistic type theory}.
    7.57  \newblock Bibliopolis, 1984.
    7.58  
    7.59 -\bibitem{milner78}
    7.60 -Robin Milner.
    7.61 -\newblock A theory of type polymorphism in programming.
    7.62 -\newblock {\em Journal of Computer and System Sciences}, 17:348--375, 1978.
    7.63 -
    7.64 -\bibitem{milner-coind}
    7.65 -Robin Milner and Mads Tofte.
    7.66 -\newblock Co-induction in relational semantics.
    7.67 -\newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
    7.68 -
    7.69 -\bibitem{Naraschewski-Wenzel:1998:TPHOL}
    7.70 -Wolfgang Naraschewski and Markus Wenzel.
    7.71 -\newblock Object-oriented verification based on record subtyping in
    7.72 -  higher-order logic.
    7.73 -\newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in
    7.74 -  Higher Order Logics: {TPHOLs} '98}, LNCS 1479, pages 349--366, 1998.
    7.75 -
    7.76 -\bibitem{nazareth-nipkow}
    7.77 -Dieter Nazareth and Tobias Nipkow.
    7.78 -\newblock Formal verification of algorithm {W}: The monomorphic case.
    7.79 -\newblock In von Wright et~al. \cite{tphols96}, pages 331--345.
    7.80 -
    7.81 -\bibitem{Nipkow-CR}
    7.82 -Tobias Nipkow.
    7.83 -\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}).
    7.84 -\newblock In Michael McRobbie and John~K. Slaney, editors, {\em Automated
    7.85 -  Deduction --- {CADE}-13 International Conference}, LNAI 1104, pages 733--747.
    7.86 -  Springer, 1996.
    7.87 -
    7.88 -\bibitem{nipkow-IMP}
    7.89 -Tobias Nipkow.
    7.90 -\newblock Winskel is (almost) right: Towards a mechanized semantics textbook.
    7.91 -\newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software
    7.92 -  Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS},
    7.93 -  pages 180--192. Springer, 1996.
    7.94 -
    7.95  \bibitem{nordstrom90}
    7.96  Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
    7.97  \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
    7.98  \newblock Oxford University Press, 1990.
    7.99  
   7.100 -\bibitem{paulson85}
   7.101 -Lawrence~C. Paulson.
   7.102 -\newblock Verifying the unification algorithm in {LCF}.
   7.103 -\newblock {\em Science of Computer Programming}, 5:143--170, 1985.
   7.104 -
   7.105  \bibitem{paulson87}
   7.106  Lawrence~C. Paulson.
   7.107  \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
   7.108  \newblock Cambridge University Press, 1987.
   7.109  
   7.110 -\bibitem{paulson-CADE}
   7.111 -Lawrence~C. Paulson.
   7.112 -\newblock A fixedpoint approach to implementing (co)inductive definitions.
   7.113 -\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12
   7.114 -  International Conference}, LNAI 814, pages 148--161. Springer, 1994.
   7.115 -
   7.116 -\bibitem{paulson-set-II}
   7.117 -Lawrence~C. Paulson.
   7.118 -\newblock Set theory for verification: {II}. {Induction} and recursion.
   7.119 -\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
   7.120 -
   7.121 -\bibitem{paulson-ns}
   7.122 -Lawrence~C. Paulson.
   7.123 -\newblock Mechanized proofs of security protocols: {Needham-Schroeder} with
   7.124 -  public keys.
   7.125 -\newblock Technical Report 413, Computer Laboratory, University of Cambridge,
   7.126 -  January 1997.
   7.127 -
   7.128 -\bibitem{paulson-coind}
   7.129 -Lawrence~C. Paulson.
   7.130 -\newblock Mechanizing coinduction and corecursion in higher-order logic.
   7.131 -\newblock {\em Journal of Logic and Computation}, 7(2):175--204, March 1997.
   7.132 -
   7.133 -\bibitem{paulson-security}
   7.134 -Lawrence~C. Paulson.
   7.135 -\newblock Proving properties of security protocols by induction.
   7.136 -\newblock In {\em 10th Computer Security Foundations Workshop}, pages 70--83.
   7.137 -  IEEE Computer Society Press, 1997.
   7.138 -
   7.139  \bibitem{isabelle-ZF}
   7.140  Lawrence~C. Paulson.
   7.141  \newblock {Isabelle}'s logics: {FOL} and {ZF}.
   7.142  \newblock Technical report, Computer Laboratory, University of Cambridge, 1999.
   7.143  
   7.144 -\bibitem{paulson-COLOG}
   7.145 -Lawrence~C. Paulson.
   7.146 -\newblock A formulation of the simple theory of types (for {Isabelle}).
   7.147 -\newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
   7.148 -  International Conference on Computer Logic}, LNCS 417, pages 246--274,
   7.149 -  Tallinn, Published 1990. Estonian Academy of Sciences, Springer.
   7.150 -
   7.151  \bibitem{pelletier86}
   7.152  F.~J. Pelletier.
   7.153  \newblock Seventy-five problems for testing automatic theorem provers.
   7.154  \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
   7.155  \newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
   7.156  
   7.157 -\bibitem{plaisted90}
   7.158 -David~A. Plaisted.
   7.159 -\newblock A sequent-style model elimination strategy and a positive refinement.
   7.160 -\newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990.
   7.161 -
   7.162 -\bibitem{slind-tfl}
   7.163 -Konrad Slind.
   7.164 -\newblock Function definition in higher-order logic.
   7.165 -\newblock In von Wright et~al. \cite{tphols96}.
   7.166 -
   7.167  \bibitem{takeuti87}
   7.168  G.~Takeuti.
   7.169  \newblock {\em Proof Theory}.
   7.170 @@ -189,14 +74,4 @@
   7.171  \newblock {\em Type Theory and Functional Programming}.
   7.172  \newblock Addison-Wesley, 1991.
   7.173  
   7.174 -\bibitem{tphols96}
   7.175 -J.~von Wright, J.~Grundy, and J.~Harrison, editors.
   7.176 -\newblock {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96}, LNCS
   7.177 -  1125, 1996.
   7.178 -
   7.179 -\bibitem{winskel93}
   7.180 -Glynn Winskel.
   7.181 -\newblock {\em The Formal Semantics of Programming Languages}.
   7.182 -\newblock MIT Press, 1993.
   7.183 -
   7.184  \end{thebibliography}
     8.1 --- a/doc-src/Logics/logics.tex	Wed May 05 14:31:31 1999 +0200
     8.2 +++ b/doc-src/Logics/logics.tex	Wed May 05 16:44:42 1999 +0200
     8.3 @@ -53,6 +53,6 @@
     8.4  %%\include{Cube}
     8.5  %%\include{LCF}
     8.6  \bibliographystyle{plain}
     8.7 -\bibliography{bib,string,general,atp,theory,funprog,logicprog,isabelle,crossref}
     8.8 +\bibliography{../manual}
     8.9  \input{logics.ind}
    8.10  \end{document}
     9.1 --- a/doc-src/Ref/classical.tex	Wed May 05 14:31:31 1999 +0200
     9.2 +++ b/doc-src/Ref/classical.tex	Wed May 05 16:44:42 1999 +0200
     9.3 @@ -112,7 +112,7 @@
     9.4  theorem and apply rules backwards in a fairly arbitrary manner.  This yields a
     9.5  surprisingly effective proof procedure.  Quantifiers add few complications,
     9.6  since Isabelle handles parameters and schematic variables.  See Chapter~10
     9.7 -of {\em ML for the Working Programmer}~\cite{paulson91} for further
     9.8 +of {\em ML for the Working Programmer}~\cite{paulson-ml2} for further
     9.9  discussion.
    9.10  
    9.11  
    10.1 --- a/doc-src/Ref/defining.tex	Wed May 05 14:31:31 1999 +0200
    10.2 +++ b/doc-src/Ref/defining.tex	Wed May 05 16:44:42 1999 +0200
    10.3 @@ -584,7 +584,7 @@
    10.4  space and followed by a space or line break; the entire phrase is a pretty
    10.5  printing block.  Other examples appear in Fig.\ts\ref{fig:set_trans} below.
    10.6  Isabelle's pretty printer resembles the one described in
    10.7 -Paulson~\cite{paulson91}.
    10.8 +Paulson~\cite{paulson-ml2}.
    10.9  
   10.10  \index{pretty printing|)}
   10.11  
    11.1 --- a/doc-src/Ref/ref.bbl	Wed May 05 14:31:31 1999 +0200
    11.2 +++ b/doc-src/Ref/ref.bbl	Wed May 05 16:44:42 1999 +0200
    11.3 @@ -44,11 +44,6 @@
    11.4  \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
    11.5  \newblock Oxford University Press, 1990.
    11.6  
    11.7 -\bibitem{paulson91}
    11.8 -Lawrence~C. Paulson.
    11.9 -\newblock {\em {ML} for the Working Programmer}.
   11.10 -\newblock Cambridge University Press, 1991.
   11.11 -
   11.12  \bibitem{paulson-ml2}
   11.13  Lawrence~C. Paulson.
   11.14  \newblock {\em {ML} for the Working Programmer}.
    12.1 --- a/doc-src/Ref/ref.tex	Wed May 05 14:31:31 1999 +0200
    12.2 +++ b/doc-src/Ref/ref.tex	Wed May 05 16:44:42 1999 +0200
    12.3 @@ -63,7 +63,7 @@
    12.4  
    12.5  \begingroup
    12.6    \bibliographystyle{plain} \small\raggedright\frenchspacing
    12.7 -  \bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref}
    12.8 +  \bibliography{../manual}
    12.9  \endgroup
   12.10  \include{theory-syntax}
   12.11  
    13.1 --- a/doc-src/Ref/theories.tex	Wed May 05 14:31:31 1999 +0200
    13.2 +++ b/doc-src/Ref/theories.tex	Wed May 05 16:44:42 1999 +0200
    13.3 @@ -486,7 +486,7 @@
    13.4    number of lambdas, starting from zero, between a variable's occurrence
    13.5    and its binding.  The representation prevents capture of variables.  For
    13.6    more information see de Bruijn \cite{debruijn72} or
    13.7 -  Paulson~\cite[page~336]{paulson91}.
    13.8 +  Paulson~\cite[page~376]{paulson-ml2}.
    13.9  
   13.10  \item[\ttindexbold{Abs} ($a$, $T$, $u$)]
   13.11    \index{lambda abs@$\lambda$-abstractions|bold}
    14.1 --- a/doc-src/ZF/ZF.tex	Wed May 05 14:31:31 1999 +0200
    14.2 +++ b/doc-src/ZF/ZF.tex	Wed May 05 16:44:42 1999 +0200
    14.3 @@ -31,7 +31,7 @@
    14.4  Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF}
    14.5  less formally than this chapter.  Isabelle employs a novel treatment of
    14.6  non-well-founded data structures within the standard {\sc zf} axioms including
    14.7 -the Axiom of Foundation~\cite{paulson-final}.
    14.8 +the Axiom of Foundation~\cite{paulson-mscs}.
    14.9  
   14.10  
   14.11  \section{Which version of axiomatic set theory?}
   14.12 @@ -1116,7 +1116,7 @@
   14.13  non-standard notion of disjoint sum using non-standard pairs.  All of these
   14.14  concepts satisfy the same properties as their standard counterparts; in
   14.15  addition, {\tt<$a$;$b$>} is continuous.  The theory supports coinductive
   14.16 -definitions, for example of infinite lists~\cite{paulson-final}.
   14.17 +definitions, for example of infinite lists~\cite{paulson-mscs}.
   14.18  
   14.19  \begin{figure}
   14.20  \begin{ttbox}
   14.21 @@ -2386,10 +2386,10 @@
   14.22    induction.
   14.23  
   14.24  \item Theory \texttt{ListN} inductively defines the lists of $n$
   14.25 -  elements~\cite{paulin92}.
   14.26 +  elements~\cite{paulin-tlca}.
   14.27  
   14.28  \item Theory \texttt{Acc} inductively defines the accessible part of a
   14.29 -  relation~\cite{paulin92}.
   14.30 +  relation~\cite{paulin-tlca}.
   14.31  
   14.32  \item Theory \texttt{Comb} defines the datatype of combinators and
   14.33    inductively defines contraction and parallel contraction.  It goes on to
    15.1 --- a/doc-src/ZF/logics-ZF.bbl	Wed May 05 14:31:31 1999 +0200
    15.2 +++ b/doc-src/ZF/logics-ZF.bbl	Wed May 05 16:44:42 1999 +0200
    15.3 @@ -16,7 +16,7 @@
    15.4  Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and
    15.5    Lawrence Wos.
    15.6  \newblock Set theory in first-order logic: Clauses for {G\"{o}del's} axioms.
    15.7 -\newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986.
    15.8 +\newblock {\em J. Auto. Reas.}, 2(3):287--327, 1986.
    15.9  
   15.10  \bibitem{camilleri92}
   15.11  J.~Camilleri and T.~F. Melham.
   15.12 @@ -43,7 +43,7 @@
   15.13  \bibitem{dyckhoff}
   15.14  Roy Dyckhoff.
   15.15  \newblock Contraction-free sequent calculi for intuitionistic logic.
   15.16 -\newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992.
   15.17 +\newblock {\em J. Symb. Logic}, 57(3):795--807, 1992.
   15.18  
   15.19  \bibitem{halmos60}
   15.20  Paul~R. Halmos.
   15.21 @@ -58,13 +58,13 @@
   15.22  \bibitem{noel}
   15.23  Philippe No{\"e}l.
   15.24  \newblock Experimenting with {Isabelle} in {ZF} set theory.
   15.25 -\newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993.
   15.26 +\newblock {\em J. Auto. Reas.}, 10(1):15--58, 1993.
   15.27  
   15.28 -\bibitem{paulin92}
   15.29 +\bibitem{paulin-tlca}
   15.30  Christine Paulin-Mohring.
   15.31  \newblock Inductive definitions in the system {Coq}: Rules and properties.
   15.32 -\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
   15.33 -  December 1992.
   15.34 +\newblock In M.~Bezem and J.F. Groote, editors, {\em Typed Lambda Calculi and
   15.35 +  Applications}, LNCS 664, pages 328--345. Springer, 1993.
   15.36  
   15.37  \bibitem{paulson87}
   15.38  Lawrence~C. Paulson.
   15.39 @@ -74,7 +74,7 @@
   15.40  \bibitem{paulson-set-I}
   15.41  Lawrence~C. Paulson.
   15.42  \newblock Set theory for verification: {I}. {From} foundations to functions.
   15.43 -\newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993.
   15.44 +\newblock {\em J. Auto. Reas.}, 11(3):353--389, 1993.
   15.45  
   15.46  \bibitem{paulson-CADE}
   15.47  Lawrence~C. Paulson.
   15.48 @@ -82,17 +82,10 @@
   15.49  \newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12
   15.50    International Conference}, LNAI 814, pages 148--161. Springer, 1994.
   15.51  
   15.52 -\bibitem{paulson-final}
   15.53 -Lawrence~C. Paulson.
   15.54 -\newblock A concrete final coalgebra theorem for {ZF} set theory.
   15.55 -\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em
   15.56 -  Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996,
   15.57 -  pages 120--139. Springer, 1995.
   15.58 -
   15.59  \bibitem{paulson-set-II}
   15.60  Lawrence~C. Paulson.
   15.61  \newblock Set theory for verification: {II}. {Induction} and recursion.
   15.62 -\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
   15.63 +\newblock {\em J. Auto. Reas.}, 15(2):167--215, 1995.
   15.64  
   15.65  \bibitem{paulson-generic}
   15.66  Lawrence~C. Paulson.
   15.67 @@ -100,10 +93,16 @@
   15.68  \newblock In Robert Veroff, editor, {\em Automated Reasoning and its
   15.69    Applications: Essays in Honor of {Larry Wos}}, chapter~3. MIT Press, 1997.
   15.70  
   15.71 +\bibitem{paulson-mscs}
   15.72 +Lawrence~C. Paulson.
   15.73 +\newblock Final coalgebras as greatest fixed points in zf set theory.
   15.74 +\newblock {\em Mathematical Structures in Computer Science}, 9, 1999.
   15.75 +\newblock in press.
   15.76 +
   15.77  \bibitem{quaife92}
   15.78  Art Quaife.
   15.79  \newblock Automated deduction in {von Neumann-Bernays-G\"{o}del} set theory.
   15.80 -\newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992.
   15.81 +\newblock {\em J. Auto. Reas.}, 8(1):91--147, 1992.
   15.82  
   15.83  \bibitem{suppes72}
   15.84  Patrick Suppes.
    16.1 --- a/doc-src/ZF/logics-ZF.tex	Wed May 05 14:31:31 1999 +0200
    16.2 +++ b/doc-src/ZF/logics-ZF.tex	Wed May 05 16:44:42 1999 +0200
    16.3 @@ -57,6 +57,6 @@
    16.4  \include{FOL}
    16.5  \include{ZF}
    16.6  \bibliographystyle{plain}
    16.7 -\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref}
    16.8 +\bibliography{../manual}
    16.9  \input{logics-ZF.ind}
   16.10  \end{document}
    17.1 --- a/doc-src/isabelle.bib	Wed May 05 14:31:31 1999 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,58 +0,0 @@
    17.4 -@string{AP="Academic Press"}
    17.5 -@string{CUP="Cambridge University Press"}
    17.6 -@string{FAC="Formal Aspects of Computing"}
    17.7 -@string{JSL="J. Symbolic Logic"}
    17.8 -@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
    17.9 -@string{MIT="MIT Press"}
   17.10 -@string{Springer="Springer-Verlag"}
   17.11 -
   17.12 -@book{andrews86,author="Peter Andrews",
   17.13 -title="An Introduction to Mathematical Logic and Type Theory: to Truth
   17.14 -through Proof",publisher=AP,
   17.15 -series="Computer Science and Applied Mathematics",year=1986}
   17.16 -
   17.17 -@book{mgordon-hol,editor="M.J.C. Gordon and T.F. Melham",
   17.18 -title=
   17.19 -"Introduction to {HOL}: a theorem-proving environment for higher order logic",
   17.20 -publisher=CUP,year=1993}
   17.21 -
   17.22 -@article{church40,author="Alonzo Church",
   17.23 -title="A Formulation of the Simple Theory of Types",
   17.24 -journal=JSL,year=1940,volume=5,pages="56--68"}
   17.25 -
   17.26 -@article{milner78,author="Robin Milner",
   17.27 -title="A Theory of Type Polymorphism in Programming",
   17.28 -journal="J. Comp.\ Sys.\ Sci.",year=1978,volume=17,pages="348--375"}
   17.29 -
   17.30 -@InProceedings{NaraschewskiW-TPHOLs98,
   17.31 -author={Wolfgang Naraschewski and Markus Wenzel},
   17.32 -title=
   17.33 -{Object-Oriented Verification based on Record Subtyping in Higher-Order Logic},
   17.34 -booktitle={Theorem Proving in Higher Order Logics (TPHOLs'98)},
   17.35 -publisher=Springer,volume=1479,series=LNCS,year=1998}
   17.36 -
   17.37 -@inproceedings{nipkow-W,
   17.38 -author={Wolfgang Naraschewski and Tobias Nipkow},
   17.39 -title={Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
   17.40 -booktitle={Types for Proofs and Programs: Intl. Workshop TYPES '96},
   17.41 -editor={E. Gim\'enez and C. Paulin-Mohring},
   17.42 -publisher=Springer,series=LNCS,volume=1512,pages={317--332},year=1998}
   17.43 -
   17.44 -@inproceedings{Nipkow-CR,author={Tobias Nipkow},
   17.45 -title={More {Church-Rosser} Proofs (in {Isabelle/HOL})},
   17.46 -booktitle={Automated Deduction --- CADE-13},
   17.47 -editor={M. McRobbie and J.K. Slaney},
   17.48 -publisher=Springer,series=LNCS,volume=1104,pages={733--747},year=1996}
   17.49 -
   17.50 -@article{nipkow-IMP,author={Tobias Nipkow},
   17.51 -title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
   17.52 -journal=FAC,volume=10,pages={171--186},year=1998}
   17.53 -
   17.54 -@inproceedings{slind-tfl,author={Konrad Slind},
   17.55 -title={Function Definition in Higher Order Logic},
   17.56 -booktitle={Theorem Proving in Higher Order Logics},
   17.57 -editor={J. von Wright and J. Grundy and J. Harrison},
   17.58 -publisher=Springer,series=LNCS,volume=1125,pages={381--397},year=1996}
   17.59 -
   17.60 -@book{winskel93,author={Glynn Winskel},
   17.61 -title={The Formal Semantics of Programming Languages},publisher=MIT,year=1993}
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/doc-src/manual.bib	Wed May 05 16:44:42 1999 +0200
    18.3 @@ -0,0 +1,937 @@
    18.4 +% BibTeX database for the Isabelle documentation
    18.5 +%
    18.6 +% Lawrence C Paulson $Id$
    18.7 +
    18.8 +%publishers
    18.9 +@string{AP="Academic Press"}
   18.10 +@string{CUP="Cambridge University Press"}
   18.11 +@string{IEEE="{\sc ieee} Computer Society Press"}
   18.12 +@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
   18.13 +@string{MIT="MIT Press"}
   18.14 +@string{NH="North-Holland"}
   18.15 +@string{Prentice="Prentice-Hall"}
   18.16 +@string{Springer="Springer-Verlag"}
   18.17 +
   18.18 +%institutions
   18.19 +@string{CUCL="Computer Laboratory, University of Cambridge"}
   18.20 +
   18.21 +%journals
   18.22 +@string{FAC="Formal Aspects Comput."}
   18.23 +@string{JAR="J. Auto. Reas."}
   18.24 +@string{JCS="J. Comput. Secur."}
   18.25 +@string{JFP="J. Func. Prog."}
   18.26 +@string{JLC="J. Logic and Comput."}
   18.27 +@string{JLP="J. Logic Prog."}
   18.28 +@string{JSC="J. Symb. Comput."}
   18.29 +@string{JSL="J. Symb. Logic"}
   18.30 +@string{SIGPLAN="{SIGPLAN} Notices"}
   18.31 +
   18.32 +%conferences
   18.33 +@string{CADE="International Conference on Automated Deduction"}
   18.34 +@string{POPL="Symposium on Principles of Programming Languages"}
   18.35 +@string{TYPES="Types for Proofs and Programs"}
   18.36 +
   18.37 +
   18.38 +%A
   18.39 +
   18.40 +@incollection{abramsky90,
   18.41 +  author	= {Samson Abramsky},
   18.42 +  title		= {The Lazy Lambda Calculus},
   18.43 +  pages		= {65-116},
   18.44 +  editor	= {David A. Turner},
   18.45 +  booktitle	= {Research Topics in Functional Programming},
   18.46 +  publisher	= {Addison-Wesley},
   18.47 +  year		= 1990}
   18.48 +
   18.49 +@Unpublished{abrial93,
   18.50 +  author	= {J. R. Abrial and G. Laffitte},
   18.51 +  title		= {Towards the Mechanization of the Proofs of some Classical
   18.52 +		  Theorems of Set Theory},
   18.53 +  note		= {preprint},
   18.54 +  year		= 1993,
   18.55 +  month		= Feb}
   18.56 +
   18.57 +@incollection{aczel77,
   18.58 +  author	= {Peter Aczel},
   18.59 +  title		= {An Introduction to Inductive Definitions},
   18.60 +  pages		= {739-782},
   18.61 +  crossref	= {barwise-handbk}}
   18.62 +
   18.63 +@Book{aczel88,
   18.64 +  author	= {Peter Aczel},
   18.65 +  title		= {Non-Well-Founded Sets},
   18.66 +  publisher	= {CSLI},
   18.67 +  year		= 1988}
   18.68 +
   18.69 +@InProceedings{alf,
   18.70 +  author	= {Lena Magnusson and Bengt {Nordstr\"{o}m}},
   18.71 +  title		= {The {ALF} Proof Editor and Its Proof Engine},
   18.72 +  crossref	= {types93},
   18.73 +  pages		= {213-237}}
   18.74 +
   18.75 +@book{andrews86,
   18.76 +  author	= "Peter Andrews",
   18.77 +  title		= "An Introduction to Mathematical Logic and Type Theory: to Truth
   18.78 +through Proof",
   18.79 +  publisher	= AP,
   18.80 +  series	= "Computer Science and Applied Mathematics",
   18.81 +  year		= 1986}
   18.82 +
   18.83 +%B
   18.84 +
   18.85 +@incollection{basin91,
   18.86 +  author	= {David Basin and Matt Kaufmann},
   18.87 +  title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
   18.88 +		   Comparison}, 
   18.89 +  crossref	= {huet-plotkin91},
   18.90 +  pages		= {89-119}}
   18.91 +
   18.92 +@Article{boyer86,
   18.93 +  author	= {Robert Boyer and Ewing Lusk and William McCune and Ross
   18.94 +		   Overbeek and Mark Stickel and Lawrence Wos},
   18.95 +  title		= {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}
   18.96 +		   Axioms},
   18.97 +  journal	= JAR,
   18.98 +  year		= 1986,
   18.99 +  volume	= 2,
  18.100 +  number	= 3,
  18.101 +  pages		= {287-327}}
  18.102 +
  18.103 +@book{bm79,
  18.104 +  author	= {Robert S. Boyer and J Strother Moore},
  18.105 +  title		= {A Computational Logic},
  18.106 +  publisher	= {Academic Press},
  18.107 +  year		= 1979}
  18.108 +
  18.109 +@book{bm88book,
  18.110 +  author	= {Robert S. Boyer and J Strother Moore},
  18.111 +  title		= {A Computational Logic Handbook},
  18.112 +  publisher	= {Academic Press},
  18.113 +  year		= 1988}
  18.114 +
  18.115 +@Article{debruijn72,
  18.116 +  author	= {N. G. de Bruijn},
  18.117 +  title		= {Lambda Calculus Notation with Nameless Dummies,
  18.118 +	a Tool for Automatic Formula Manipulation,
  18.119 +	with Application to the {Church-Rosser Theorem}},
  18.120 +  journal	= {Indag. Math.},
  18.121 +  volume	= 34,
  18.122 +  pages		= {381-392},
  18.123 +  year		= 1972}
  18.124 +
  18.125 +%C
  18.126 +
  18.127 +@TechReport{camilleri92,
  18.128 +  author	= {J. Camilleri and T. F. Melham},
  18.129 +  title		= {Reasoning with Inductively Defined Relations in the
  18.130 +		 {HOL} Theorem Prover},
  18.131 +  institution	= CUCL,
  18.132 +  year		= 1992,
  18.133 +  number	= 265,
  18.134 +  month		= Aug}
  18.135 +
  18.136 +@Book{charniak80,
  18.137 +  author	= {E. Charniak and C. K. Riesbeck and D. V. McDermott},
  18.138 +  title		= {Artificial Intelligence Programming},
  18.139 +  publisher	= {Lawrence Erlbaum Associates},
  18.140 +  year		= 1980}
  18.141 +
  18.142 +@article{church40,
  18.143 +  author	= "Alonzo Church",
  18.144 +  title		= "A Formulation of the Simple Theory of Types",
  18.145 +  journal	= JSL,
  18.146 +  year		= 1940,
  18.147 +  volume	= 5,
  18.148 +  pages		= "56-68"}
  18.149 +
  18.150 +@PhdThesis{coen92,
  18.151 +  author	= {Martin D. Coen},
  18.152 +  title		= {Interactive Program Derivation},
  18.153 +  school	= {University of Cambridge},
  18.154 +  note		= {Computer Laboratory Technical Report 272},
  18.155 +  month		= nov,
  18.156 +  year		= 1992}
  18.157 +
  18.158 +@book{constable86,
  18.159 +  author	= {R. L. Constable and others},
  18.160 +  title		= {Implementing Mathematics with the Nuprl Proof
  18.161 +		 Development System}, 
  18.162 +  publisher	= Prentice,
  18.163 +  year		= 1986}
  18.164 +
  18.165 +%D
  18.166 +
  18.167 +@Book{davey&priestley,
  18.168 +  author	= {B. A. Davey and H. A. Priestley},
  18.169 +  title		= {Introduction to Lattices and Order},
  18.170 +  publisher	= CUP,
  18.171 +  year		= 1990}
  18.172 +
  18.173 +@Book{devlin79,
  18.174 +  author	= {Keith J. Devlin},
  18.175 +  title		= {Fundamentals of Contemporary Set Theory},
  18.176 +  publisher	= {Springer},
  18.177 +  year		= 1979}
  18.178 +
  18.179 +@book{dummett,
  18.180 +  author	= {Michael Dummett},
  18.181 +  title		= {Elements of Intuitionism},
  18.182 +  year		= 1977,
  18.183 +  publisher	= {Oxford University Press}}
  18.184 +
  18.185 +@incollection{dybjer91,
  18.186 +  author	= {Peter Dybjer},
  18.187 +  title		= {Inductive Sets and Families in {Martin-L\"of's} Type
  18.188 +		  Theory and Their Set-Theoretic Semantics}, 
  18.189 +  crossref	= {huet-plotkin91},
  18.190 +  pages		= {280-306}}
  18.191 +
  18.192 +@Article{dyckhoff,
  18.193 +  author	= {Roy Dyckhoff},
  18.194 +  title		= {Contraction-Free Sequent Calculi for Intuitionistic Logic},
  18.195 +  journal	= JSL,
  18.196 +  year		= 1992,
  18.197 +  volume	= 57,
  18.198 +  number	= 3,
  18.199 +  pages		= {795-807}}
  18.200 +
  18.201 +%F
  18.202 +
  18.203 +@InProceedings{felty91a,
  18.204 +  Author	= {Amy Felty},
  18.205 +  Title		= {A Logic Program for Transforming Sequent Proofs to Natural
  18.206 +		  Deduction Proofs}, 
  18.207 +  crossref	= {extensions91},
  18.208 +  pages		= {157-178}}
  18.209 +
  18.210 +@TechReport{frost93,
  18.211 +  author	= {Jacob Frost},
  18.212 +  title		= {A Case Study of Co-induction in {Isabelle HOL}},
  18.213 +  institution	= CUCL,
  18.214 +  number	= 308,
  18.215 +  year		= 1993,
  18.216 +  month		= Aug}
  18.217 +
  18.218 +%revised version of frost93
  18.219 +@TechReport{frost95,
  18.220 +  author	= {Jacob Frost},
  18.221 +  title		= {A Case Study of Co-induction in {Isabelle}},
  18.222 +  institution	= CUCL,
  18.223 +  number	= 359,
  18.224 +  year		= 1995,
  18.225 +  month		= Feb}
  18.226 +
  18.227 +@inproceedings{OBJ,
  18.228 +  author	= {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
  18.229 +		 and J. Meseguer}, 
  18.230 +  title		= {Principles of {OBJ2}},
  18.231 +  booktitle	= POPL, 
  18.232 +  year		= 1985,
  18.233 +  pages		= {52-66}}
  18.234 +
  18.235 +%G
  18.236 +
  18.237 +@book{gallier86,
  18.238 +  author	= {J. H. Gallier},
  18.239 +  title		= {Logic for Computer Science: 
  18.240 +		Foundations of Automatic Theorem Proving},
  18.241 +  year		= 1986,
  18.242 +  publisher	= {Harper \& Row}}
  18.243 +
  18.244 +@Book{galton90,
  18.245 +  author	= {Antony Galton},
  18.246 +  title		= {Logic for Information Technology},
  18.247 +  publisher	= {Wiley},
  18.248 +  year		= 1990}
  18.249 +
  18.250 +@InProceedings{gimenez-codifying,
  18.251 +  author	= {Eduardo Gim{\'e}nez},
  18.252 +  title		= {Codifying Guarded Definitions with Recursive Schemes},
  18.253 +  crossref	= {types94},
  18.254 +  pages		= {39-59}
  18.255 +}
  18.256 +
  18.257 +@Book{mgordon-hol,
  18.258 +  author	= {M. J. C. Gordon and T. F. Melham},
  18.259 +  title		= {Introduction to {HOL}: A Theorem Proving Environment for
  18.260 +		 Higher Order Logic},
  18.261 +  publisher	= CUP,
  18.262 +  year		= 1993}
  18.263 +
  18.264 +@book{mgordon79,
  18.265 +  author	= {Michael J. C. Gordon and Robin Milner and Christopher P.
  18.266 +		 Wadsworth},
  18.267 +  title		= {Edinburgh {LCF}: A Mechanised Logic of Computation},
  18.268 +  year		= 1979,
  18.269 +  publisher	= {Springer},
  18.270 +  series	= {LNCS 78}}
  18.271 +
  18.272 +@InProceedings{gunter-trees,
  18.273 +  author	= {Elsa L. Gunter},
  18.274 +  title		= {A Broader Class of Trees for Recursive Type Definitions for
  18.275 +		  {HOL}},
  18.276 +  crossref	= {hug93},
  18.277 +  pages		= {141-154}}
  18.278 +
  18.279 +%H
  18.280 +
  18.281 +@Book{halmos60,
  18.282 +  author	= {Paul R. Halmos},
  18.283 +  title		= {Naive Set Theory},
  18.284 +  publisher	= {Van Nostrand},
  18.285 +  year		= 1960}
  18.286 +
  18.287 +@Book{hennessy90,
  18.288 +  author	= {Matthew Hennessy},
  18.289 +  title		= {The Semantics of Programming Languages: An Elementary
  18.290 +		  Introduction Using Structural Operational Semantics},
  18.291 +  publisher	= {Wiley},
  18.292 +  year		= 1990}
  18.293 +
  18.294 +@Article{haskell-report,
  18.295 +  author	= {Paul Hudak and Simon Peyton Jones and Philip Wadler},
  18.296 +  title		= {Report on the Programming Language {Haskell}: A
  18.297 +		 Non-strict, Purely Functional Language},
  18.298 +  journal	= SIGPLAN,
  18.299 +  year		= 1992,
  18.300 +  volume	= 27,
  18.301 +  number	= 5,
  18.302 +  month		= May,
  18.303 +  note		= {Version 1.2}}
  18.304 +
  18.305 +@Article{haskell-tutorial,
  18.306 +  author	= {Paul Hudak and Joseph H. Fasel},
  18.307 +  title		= {A Gentle Introduction to {Haskell}},
  18.308 +  journal	= SIGPLAN,
  18.309 +  year		= 1992,
  18.310 +  volume	= 27,
  18.311 +  number	= 5,
  18.312 +  month		= May}
  18.313 +
  18.314 +@article{huet75,
  18.315 +  author	= {G. P. Huet},
  18.316 +  title		= {A Unification Algorithm for Typed $\lambda$-Calculus},
  18.317 +  journal	= TCS,
  18.318 +  volume	= 1,
  18.319 +  year		= 1975,
  18.320 +  pages		= {27-57}}
  18.321 +
  18.322 +@article{huet78,
  18.323 +  author	= {G. P. Huet and B. Lang},
  18.324 +  title		= {Proving and Applying Program Transformations Expressed with 
  18.325 +			Second-Order Patterns},
  18.326 +  journal	= acta,
  18.327 +  volume	= 11,
  18.328 +  year		= 1978, 
  18.329 +  pages		= {31-55}}
  18.330 +
  18.331 +@inproceedings{huet88,
  18.332 +  author	= {G\'erard Huet},
  18.333 +  title		= {Induction Principles Formalized in the {Calculus of
  18.334 +		 Constructions}}, 
  18.335 +  booktitle	= {Programming of Future Generation Computers},
  18.336 +  editor	= {K. Fuchi and M. Nivat},
  18.337 +  year		= 1988,
  18.338 +  pages		= {205-216}, 
  18.339 +  publisher	= {Elsevier}}
  18.340 +
  18.341 +%K
  18.342 +
  18.343 +@Book{kunen80,
  18.344 +  author	= {Kenneth Kunen},
  18.345 +  title		= {Set Theory: An Introduction to Independence Proofs},
  18.346 +  publisher	= NH,
  18.347 +  year		= 1980}
  18.348 +
  18.349 +%M
  18.350 +
  18.351 +@Article{mw81,
  18.352 +  author	= {Zohar Manna and Richard Waldinger},
  18.353 +  title		= {Deductive Synthesis of the Unification Algorithm},
  18.354 +  journal	= SCP,
  18.355 +  year		= 1981,
  18.356 +  volume	= 1,
  18.357 +  number	= 1,
  18.358 +  pages		= {5-48}}
  18.359 +
  18.360 +@InProceedings{martin-nipkow,
  18.361 +  author	= {Ursula Martin and Tobias Nipkow},
  18.362 +  title		= {Ordered Rewriting and Confluence},
  18.363 +  crossref	= {cade10},
  18.364 +  pages		= {366-380}}
  18.365 +
  18.366 +@book{martinlof84,
  18.367 +  author	= {Per Martin-L\"of},
  18.368 +  title		= {Intuitionistic type theory},
  18.369 +  year		= 1984,
  18.370 +  publisher	= {Bibliopolis}}
  18.371 +
  18.372 +@incollection{melham89,
  18.373 +  author	= {Thomas F. Melham},
  18.374 +  title		= {Automating Recursive Type Definitions in Higher Order
  18.375 +		 Logic}, 
  18.376 +  pages		= {341-386},
  18.377 +  crossref	= {birtwistle89}}
  18.378 +
  18.379 +@Article{miller-mixed,
  18.380 +  Author	= {Dale Miller},
  18.381 +  Title		= {Unification Under a Mixed Prefix},
  18.382 +  journal	= JSC,
  18.383 +  volume	= 14,
  18.384 +  number	= 4,
  18.385 +  pages		= {321-358},
  18.386 +  Year		= 1992}
  18.387 +
  18.388 +@Article{milner78,
  18.389 +  author	= {Robin Milner},
  18.390 +  title		= {A Theory of Type Polymorphism in Programming},
  18.391 +  journal	= "J. Comp.\ Sys.\ Sci.",
  18.392 +  year		= 1978,
  18.393 +  volume	= 17,
  18.394 +  pages		= {348-375}}
  18.395 +
  18.396 +@TechReport{milner-ind,
  18.397 +  author	= {Robin Milner},
  18.398 +  title		= {How to Derive Inductions in {LCF}},
  18.399 +  institution	= Edinburgh,
  18.400 +  year		= 1980,
  18.401 +  type		= {note}}
  18.402 +
  18.403 +@Article{milner-coind,
  18.404 +  author	= {Robin Milner and Mads Tofte},
  18.405 +  title		= {Co-induction in Relational Semantics},
  18.406 +  journal	= TCS,
  18.407 +  year		= 1991,
  18.408 +  volume	= 87,
  18.409 +  pages		= {209-220}}
  18.410 +
  18.411 +@Book{milner89,
  18.412 +  author	= {Robin Milner},
  18.413 +  title		= {Communication and Concurrency},
  18.414 +  publisher	= Prentice,
  18.415 +  year		= 1989}
  18.416 +
  18.417 +@PhdThesis{monahan84,
  18.418 +  author	= {Brian Q. Monahan},
  18.419 +  title		= {Data Type Proofs using Edinburgh {LCF}},
  18.420 +  school	= {University of Edinburgh},
  18.421 +  year		= 1984}
  18.422 +
  18.423 +%N
  18.424 +
  18.425 +@InProceedings{NaraschewskiW-TPHOLs98,
  18.426 +  author	= {Wolfgang Naraschewski and Markus Wenzel},
  18.427 +  title		= 
  18.428 +{Object-Oriented Verification based on Record Subtyping in Higher-Order Logic},
  18.429 +  booktitle	= {Theorem Proving in Higher Order Logics (TPHOLs'98)},
  18.430 +  publisher	= Springer,
  18.431 +  volume	= 1479,
  18.432 +  series	= LNCS,
  18.433 +  year		= 1998}
  18.434 +
  18.435 +@inproceedings{nazareth-nipkow,
  18.436 +  author	= {Dieter Nazareth and Tobias Nipkow},
  18.437 +  title		= {Formal Verification of Algorithm {W}: The Monomorphic Case},
  18.438 +  crossref	= {tphols96},
  18.439 +  pages		= {331-345},
  18.440 +  year		= 1996}
  18.441 +
  18.442 +@inproceedings{nipkow-W,
  18.443 +  author	= {Wolfgang Naraschewski and Tobias Nipkow},
  18.444 +  title		= {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
  18.445 +  booktitle	= {Types for Proofs and Programs: Intl. Workshop TYPES '96},
  18.446 +  editor	= {E. Gim\'enez and C. Paulin-Mohring},
  18.447 +  publisher	= Springer,
  18.448 +  series	= LNCS,
  18.449 +  volume	= 1512,
  18.450 +  pages		= {317-332},
  18.451 +  year		= 1998}
  18.452 +
  18.453 +@inproceedings{Nipkow-CR,
  18.454 +  author	= {Tobias Nipkow},
  18.455 +  title		= {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
  18.456 +  booktitle	= {Automated Deduction --- CADE-13},
  18.457 +  editor	= {M. McRobbie and J.K. Slaney},
  18.458 +  publisher	= Springer,
  18.459 +  series	= LNCS,
  18.460 +  volume	= 1104,
  18.461 +  pages		= {733-747},
  18.462 +  year		= 1996}
  18.463 +
  18.464 +% WAS Nipkow-LICS-93
  18.465 +@InProceedings{nipkow-patterns,
  18.466 +  title		= {Functional Unification of Higher-Order Patterns},
  18.467 +  author	= {Tobias Nipkow},
  18.468 +  pages		= {64-74},
  18.469 +  crossref	= {lics8},
  18.470 +  url		= {ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html},
  18.471 +  keywords	= {unification}}
  18.472 +
  18.473 +@article{nipkow-IMP,
  18.474 +  author	= {Tobias Nipkow},
  18.475 +  title		= {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
  18.476 +  journal	= FAC,
  18.477 +  volume	= 10,
  18.478 +  pages		= {171-186},
  18.479 +  year		= 1998}
  18.480 +
  18.481 +@article{nipkow-prehofer,
  18.482 +  author	= {Tobias Nipkow and Christian Prehofer},
  18.483 +  title		= {Type Reconstruction for Type Classes},
  18.484 +  journal	= JFP,
  18.485 +  volume	= 5,
  18.486 +  number	= 2,
  18.487 +  year		= 1995,
  18.488 +  pages		= {201-224}}
  18.489 +
  18.490 +@Article{noel,
  18.491 +  author	= {Philippe No{\"e}l},
  18.492 +  title		= {Experimenting with {Isabelle} in {ZF} Set Theory},
  18.493 +  journal	= JAR,
  18.494 +  volume	= 10,
  18.495 +  number	= 1,
  18.496 +  pages		= {15-58},
  18.497 +  year		= 1993}
  18.498 +
  18.499 +@book{nordstrom90,
  18.500 +  author	= {Bengt {Nordstr\"om} and Kent Petersson and Jan Smith},
  18.501 +  title		= {Programming in {Martin-L\"of}'s Type Theory.  An
  18.502 +		 Introduction}, 
  18.503 +  publisher	= {Oxford University Press}, 
  18.504 +  year		= 1990}
  18.505 +
  18.506 +%O
  18.507 +
  18.508 +@Manual{pvs-language,
  18.509 +  title		= {The {PVS} specification language},
  18.510 +  author	= {S. Owre and N. Shankar and J. M. Rushby},
  18.511 +  organization	= {Computer Science Laboratory, SRI International},
  18.512 +  address	= {Menlo Park, CA},
  18.513 +  note		= {Beta release},
  18.514 +  year		= 1993,
  18.515 +  month		= apr,
  18.516 +  url		= {\verb|http://www.csl.sri.com/reports/pvs-language.dvi.Z|}}
  18.517 +
  18.518 +%P
  18.519 +
  18.520 +% replaces paulin92
  18.521 +@InProceedings{paulin-tlca,
  18.522 +  author	= {Christine Paulin-Mohring},
  18.523 +  title		= {Inductive Definitions in the System {Coq}: Rules and
  18.524 +		 Properties},
  18.525 +  crossref	= {tlca93},
  18.526 +  pages		= {328-345}}
  18.527 +
  18.528 +@InProceedings{paulson-CADE,
  18.529 +  author	= {Lawrence C. Paulson},
  18.530 +  title		= {A Fixedpoint Approach to Implementing (Co)Inductive
  18.531 +		  Definitions},
  18.532 +  pages		= {148-161},
  18.533 +  crossref	= {cade12}}
  18.534 +
  18.535 +@InProceedings{paulson-COLOG,
  18.536 +  author	= {Lawrence C. Paulson},
  18.537 +  title		= {A Formulation of the Simple Theory of Types (for
  18.538 +		 {Isabelle})}, 
  18.539 +  pages		= {246-274},
  18.540 +  crossref	= {colog88},
  18.541 +  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}
  18.542 +
  18.543 +@Article{paulson-coind,
  18.544 +  author	= {Lawrence C. Paulson},
  18.545 +  title		= {Mechanizing Coinduction and Corecursion in Higher-Order
  18.546 +		  Logic},
  18.547 +  journal	= JLC,
  18.548 +  year		= 1997,
  18.549 +  volume	= 7,
  18.550 +  number	= 2,
  18.551 +  month		= mar,
  18.552 +  pages		= {175-204}}
  18.553 +
  18.554 +@techreport{isabelle-ZF,
  18.555 +  author	= {Lawrence C. Paulson},
  18.556 +  title		= {{Isabelle}'s Logics: {FOL} and {ZF}},
  18.557 +  institution	= CUCL,
  18.558 +  year		= 1999}
  18.559 +
  18.560 +@article{paulson-found,
  18.561 +  author	= {Lawrence C. Paulson},
  18.562 +  title		= {The Foundation of a Generic Theorem Prover},
  18.563 +  journal	= JAR,
  18.564 +  volume	= 5,
  18.565 +  number	= 3,
  18.566 +  pages		= {363-397},
  18.567 +  year		= 1989,
  18.568 +  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}
  18.569 +
  18.570 +%replaces paulson-final
  18.571 +@Article{paulson-mscs,
  18.572 +  author	= {Lawrence C. Paulson},
  18.573 +  title		= {Final Coalgebras as Greatest Fixed Points in ZF Set Theory},
  18.574 +  journal	= {Mathematical Structures in Computer Science},
  18.575 +  year		= 1999,
  18.576 +  volume	= 9,
  18.577 +  note		= {in press}}
  18.578 +
  18.579 +@InCollection{paulson-generic,
  18.580 +  author	= {Lawrence C. Paulson},
  18.581 +  title		= {Generic Automatic Proof Tools},
  18.582 +  crossref	= {wos-fest},
  18.583 +  chapter	= 3}
  18.584 +
  18.585 +@Article{paulson-gr,
  18.586 +  author	= {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
  18.587 +  title		= {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of
  18.588 +		  Choice},
  18.589 +  journal	= JAR,
  18.590 +  year		= 1996,
  18.591 +  volume	= 17,
  18.592 +  number	= 3,
  18.593 +  month		= dec,
  18.594 +  pages		= {291-323}}
  18.595 +
  18.596 +@InCollection{paulson-handbook,
  18.597 +  author	= {Lawrence C. Paulson},
  18.598 +  title		= {Designing a Theorem Prover},
  18.599 +  crossref	= {handbk-lics2},
  18.600 +  pages		= {415-475}}
  18.601 +
  18.602 +@Book{paulson-isa-book,
  18.603 +  author	= {Lawrence C. Paulson},
  18.604 +  title		= {Isabelle: A Generic Theorem Prover},
  18.605 +  publisher	= {Springer},
  18.606 +  year		= 1994,
  18.607 +  note		= {LNCS 828}}
  18.608 +
  18.609 +@InCollection{paulson-markt,
  18.610 +  author	= {Lawrence C. Paulson},
  18.611 +  title		= {Tool Support for Logics of Programs},
  18.612 +  booktitle	= {Mathematical Methods in Program Development:
  18.613 +                  Summer School Marktoberdorf 1996},
  18.614 +  publisher	= {Springer},
  18.615 +  pages		= {461-498},
  18.616 +  year		= {Published 1997},
  18.617 +  editor	= {Manfred Broy},
  18.618 +  series	= {NATO ASI Series F}}
  18.619 +
  18.620 +%replaces Paulson-ML and paulson91
  18.621 +@book{paulson-ml2,
  18.622 +  author	= {Lawrence C. Paulson},
  18.623 +  title		= {{ML} for the Working Programmer},
  18.624 +  year		= 1996,
  18.625 +  edition	= {2nd},
  18.626 +  publisher	= CUP}
  18.627 +
  18.628 +@article{paulson-natural,
  18.629 +  author	= {Lawrence C. Paulson},
  18.630 +  title		= {Natural Deduction as Higher-order Resolution},
  18.631 +  journal	= JLP,
  18.632 +  volume	= 3,
  18.633 +  pages		= {237-258},
  18.634 +  year		= 1986,
  18.635 +  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}
  18.636 +
  18.637 +@Article{paulson-set-I,
  18.638 +  author	= {Lawrence C. Paulson},
  18.639 +  title		= {Set Theory for Verification: {I}.  {From}
  18.640 +		 Foundations to Functions},
  18.641 +  journal	= JAR,
  18.642 +  volume	= 11,
  18.643 +  number	= 3,
  18.644 +  pages		= {353-389},
  18.645 +  year		= 1993,
  18.646 +  url		= {ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}}
  18.647 +
  18.648 +@Article{paulson-set-II,
  18.649 +  author	= {Lawrence C. Paulson},
  18.650 +  title		= {Set Theory for Verification: {II}.  {Induction} and
  18.651 +		 Recursion},
  18.652 +  journal	= JAR,
  18.653 +  volume	= 15,
  18.654 +  number	= 2,
  18.655 +  pages		= {167-215},
  18.656 +  year		= 1995,
  18.657 +  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}
  18.658 +
  18.659 +@article{paulson85,
  18.660 +  author	= {Lawrence C. Paulson},
  18.661 +  title		= {Verifying the Unification Algorithm in {LCF}},
  18.662 +  journal	= SCP,
  18.663 +  volume	= 5,
  18.664 +  pages		= {143-170},
  18.665 +  year		= 1985}
  18.666 +
  18.667 +%replqces Paulson-LCF
  18.668 +@book{paulson87,
  18.669 +  author	= {Lawrence C. Paulson},
  18.670 +  title		= {Logic and Computation: Interactive proof with Cambridge
  18.671 +		 LCF}, 
  18.672 +  year		= 1987,
  18.673 +  publisher	= CUP}
  18.674 +
  18.675 +@incollection{paulson700,
  18.676 +  author	= {Lawrence C. Paulson},
  18.677 +  title		= {{Isabelle}: The Next 700 Theorem Provers},
  18.678 +  crossref	= {odifreddi90},
  18.679 +  pages		= {361-386},
  18.680 +  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}
  18.681 +
  18.682 +% replaces paulson-ns and paulson-security
  18.683 +@Article{paulson-jcs,
  18.684 +  author	= {Lawrence C. Paulson},
  18.685 +  title		= {The Inductive Approach to Verifying Cryptographic Protocols},
  18.686 +  journal	= JCS,
  18.687 +  year		= 1998,
  18.688 +  volume	= 6,
  18.689 +  pages		= {85-128}}
  18.690 +
  18.691 +@article{pelletier86,
  18.692 +  author	= {F. J. Pelletier},
  18.693 +  title		= {Seventy-five Problems for Testing Automatic Theorem
  18.694 +		 Provers}, 
  18.695 +  journal	= JAR,
  18.696 +  volume	= 2,
  18.697 +  pages		= {191-216},
  18.698 +  year		= 1986,
  18.699 +  note		= {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}}
  18.700 +
  18.701 +@Article{pitts94,  
  18.702 +  author	= {Andrew M. Pitts},
  18.703 +  title		= {A Co-induction Principle for Recursively Defined Domains},
  18.704 +  journal	= TCS,
  18.705 +  volume	= 124, 
  18.706 +  pages		= {195-219},
  18.707 +  year		= 1994} 
  18.708 +
  18.709 +@Article{plaisted90,
  18.710 +  author	= {David A. Plaisted},
  18.711 +  title		= {A Sequent-Style Model Elimination Strategy and a Positive
  18.712 +		 Refinement},
  18.713 +  journal	= JAR,
  18.714 +  year		= 1990,
  18.715 +  volume	= 6,
  18.716 +  number	= 4,
  18.717 +  pages		= {389-402}}
  18.718 +
  18.719 +%Q
  18.720 +
  18.721 +@Article{quaife92,
  18.722 +  author	= {Art Quaife},
  18.723 +  title		= {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set
  18.724 +		 Theory},
  18.725 +  journal	= JAR,
  18.726 +  year		= 1992,
  18.727 +  volume	= 8,
  18.728 +  number	= 1,
  18.729 +  pages		= {91-147}}
  18.730 +
  18.731 +%R
  18.732 +
  18.733 +@TechReport{rasmussen95,
  18.734 +  author	= {Ole Rasmussen},
  18.735 +  title		= {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting
  18.736 +		  Experiment},
  18.737 +  institution	= {Computer Laboratory, University of Cambridge},
  18.738 +  year		= 1995,
  18.739 +  number	= 364,
  18.740 +  month		= may,
  18.741 +  url		= {http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}
  18.742 +
  18.743 +@Book{reeves90,
  18.744 +  author	= {Steve Reeves and Michael Clarke},
  18.745 +  title		= {Logic for Computer Science},
  18.746 +  publisher	= {Addison-Wesley},
  18.747 +  year		= 1990}
  18.748 +
  18.749 +%S
  18.750 +
  18.751 +@inproceedings{saaltink-fme,
  18.752 +  author	= {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
  18.753 +		 Dan Craigen and Irwin Meisels},
  18.754 +  title		= {An {EVES} Data Abstraction Example}, 
  18.755 +  pages		= {578-596},
  18.756 +  crossref	= {fme93}}
  18.757 +
  18.758 +@inproceedings{slind-tfl,
  18.759 +  author	= {Konrad Slind},
  18.760 +  title		= {Function Definition in Higher Order Logic},
  18.761 +  booktitle	= {Theorem Proving in Higher Order Logics},
  18.762 +  editor	= {J. von Wright and J. Grundy and J. Harrison},
  18.763 +  publisher	= Springer,
  18.764 +  series	= LNCS,
  18.765 +  volume	= 1125,
  18.766 +  pages		= {381-397},
  18.767 +  year		= 1996}
  18.768 +
  18.769 +@book{suppes72,
  18.770 +  author	= {Patrick Suppes},
  18.771 +  title		= {Axiomatic Set Theory},
  18.772 +  year		= 1972,
  18.773 +  publisher	= {Dover}}
  18.774 +
  18.775 +@InCollection{szasz93,
  18.776 +  author	= {Nora Szasz},
  18.777 +  title		= {A Machine Checked Proof that {Ackermann's} Function is not
  18.778 +		  Primitive Recursive},
  18.779 +  crossref	= {huet-plotkin93},
  18.780 +  pages		= {317-338}}
  18.781 +
  18.782 +%T
  18.783 +
  18.784 +@book{takeuti87,
  18.785 +  author	= {G. Takeuti},
  18.786 +  title		= {Proof Theory},
  18.787 +  year		= 1987,
  18.788 +  publisher	= NH,
  18.789 +  edition	= {2nd}}
  18.790 +
  18.791 +@Book{thompson91,
  18.792 +  author	= {Simon Thompson},
  18.793 +  title		= {Type Theory and Functional Programming},
  18.794 +  publisher	= {Addison-Wesley},
  18.795 +  year		= 1991}
  18.796 +
  18.797 +%V
  18.798 +
  18.799 +@Unpublished{voelker94,
  18.800 +  author	= {Norbert V\"olker},
  18.801 +  title		= {The Verification of a Timer Program using {Isabelle/HOL}},
  18.802 +  url		= {ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz},
  18.803 +  year		= 1994,
  18.804 +  month		= aug}
  18.805 +
  18.806 +%W
  18.807 +
  18.808 +@book{principia,
  18.809 +  author	= {A. N. Whitehead and B. Russell},
  18.810 +  title		= {Principia Mathematica},
  18.811 +  year		= 1962,
  18.812 +  publisher	= CUP, 
  18.813 +  note		= {Paperback edition to *56,
  18.814 +  abridged from the 2nd edition (1927)}}
  18.815 +
  18.816 +@book{winskel93,
  18.817 +  author	= {Glynn Winskel},
  18.818 +  title		= {The Formal Semantics of Programming Languages},
  18.819 +  publisher	= MIT,year=1993}
  18.820 +
  18.821 +@InCollection{wos-bledsoe,
  18.822 +  author	= {Larry Wos},
  18.823 +  title		= {Automated Reasoning and {Bledsoe's} Dream for the Field},
  18.824 +  crossref	= {bledsoe-fest},
  18.825 +  pages		= {297-342}}
  18.826 +
  18.827 +
  18.828 +% CROSS REFERENCES
  18.829 +
  18.830 +@book{handbk-lics2,
  18.831 +  editor	= {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
  18.832 +  title		= {Handbook of Logic in Computer Science},
  18.833 +  booktitle	= {Handbook of Logic in Computer Science},
  18.834 +  publisher	= {Oxford University Press},
  18.835 +  year		= 1992,
  18.836 +  volume	= 2}
  18.837 +
  18.838 +@book{types93,
  18.839 +  editor	= {Henk Barendregt and Tobias Nipkow},
  18.840 +  title		= TYPES # {: International Workshop {TYPES '93}},
  18.841 +  booktitle	= TYPES # {: International Workshop {TYPES '93}},
  18.842 +  year		= {published 1994},
  18.843 +  publisher	= {Springer},
  18.844 +  series	= {LNCS 806}}
  18.845 +
  18.846 +@Proceedings{tlca93,
  18.847 +  title		= {Typed Lambda Calculi and Applications},
  18.848 +  booktitle	= {Typed Lambda Calculi and Applications},
  18.849 +  editor	= {M. Bezem and J.F. Groote},
  18.850 +  year		= 1993,
  18.851 +  publisher	= {Springer},
  18.852 +  series	= {LNCS 664}}
  18.853 +
  18.854 +@book{bledsoe-fest,
  18.855 +  title		= {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
  18.856 +  booktitle	= {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
  18.857 +  publisher	= {Kluwer Academic Publishers},
  18.858 +  year		= 1991,
  18.859 +  editor	= {Robert S. Boyer}}
  18.860 +
  18.861 +@Proceedings{cade12,
  18.862 +  editor	= {Alan Bundy},
  18.863 +  title		= {Automated Deduction --- {CADE}-12 
  18.864 +		  International Conference},
  18.865 +  booktitle	= {Automated Deduction --- {CADE}-12 
  18.866 +		  International Conference},
  18.867 +  year		= 1994,
  18.868 +  series	= {LNAI 814},
  18.869 +  publisher	= {Springer}}
  18.870 +
  18.871 +@book{types94,
  18.872 +  editor	= {Peter Dybjer and Bengt Nordstr{\"om} and Jan Smith},
  18.873 +  title		= TYPES # {: International Workshop {TYPES '94}},
  18.874 +  booktitle	= TYPES # {: International Workshop {TYPES '94}},
  18.875 +  year		= 1995,
  18.876 +  publisher	= {Springer},
  18.877 +  series	= {LNCS 996}}
  18.878 +
  18.879 +@book{huet-plotkin91,
  18.880 +  editor	= {{G\'erard} Huet and Gordon Plotkin},
  18.881 +  title		= {Logical Frameworks},
  18.882 +  booktitle	= {Logical Frameworks},
  18.883 +  publisher	= CUP,
  18.884 +  year		= 1991}
  18.885 +
  18.886 +@proceedings{colog88,
  18.887 +  editor	= {P. Martin-L\"of and G. Mints},
  18.888 +  title		= {COLOG-88: International Conference on Computer Logic},
  18.889 +  booktitle	= {COLOG-88: International Conference on Computer Logic},
  18.890 +  year		= {Published 1990},
  18.891 +  publisher	= {Springer},
  18.892 +  organization	= {Estonian Academy of Sciences},
  18.893 +  address	= {Tallinn},
  18.894 +  series	= {LNCS 417}}
  18.895 +
  18.896 +@book{odifreddi90,
  18.897 +  editor	= {P. Odifreddi},
  18.898 +  title		= {Logic and Computer Science},
  18.899 +  booktitle	= {Logic and Computer Science},
  18.900 +  publisher	= {Academic Press},
  18.901 +  year		= 1990}
  18.902 +
  18.903 +@proceedings{extensions91,
  18.904 +  editor	= {Peter Schroeder-Heister},
  18.905 +  title		= {Extensions of Logic Programming},
  18.906 +  booktitle	= {Extensions of Logic Programming},
  18.907 +  year		= 1991,
  18.908 +  series	= {LNAI 475}, 
  18.909 +  publisher	= {Springer}}
  18.910 +
  18.911 +@proceedings{cade10,
  18.912 +  editor	= {Mark E. Stickel},
  18.913 +  title		= {10th } # CADE,
  18.914 +  booktitle	= {10th } # CADE,
  18.915 +  year		= 1990,
  18.916 +  publisher	= {Springer},
  18.917 +  series	= {LNAI 449}}
  18.918 +
  18.919 +@Proceedings{lics8,
  18.920 +  editor	= {M. Vardi},
  18.921 +  title		= {Eighth Annual Symposium on Logic in Computer Science},
  18.922 +  booktitle	= {Eighth Annual Symposium on Logic in Computer Science},
  18.923 +  publisher	= IEEE,
  18.924 +  year		= 1993}
  18.925 +
  18.926 +@book{wos-fest,
  18.927 +  title		= {Automated Reasoning and its Applications: 
  18.928 +			Essays in Honor of {Larry Wos}},
  18.929 +  booktitle	= {Automated Reasoning and its Applications: 
  18.930 +			Essays in Honor of {Larry Wos}},
  18.931 +  publisher	= {MIT Press},
  18.932 +  year		= 1997,
  18.933 +  editor	= {Robert Veroff}}
  18.934 +
  18.935 +@Proceedings{tphols96,
  18.936 +  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
  18.937 +  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
  18.938 +  editor	= {J. von Wright and J. Grundy and J. Harrison},
  18.939 +  series	= {LNCS 1125},
  18.940 +  year		= 1996}