# HG changeset patch
# User wenzelm
# Date 925837738 -7200
# Node ID a1bb7a7b6205edac7707fc3ac2a6946cce1e3a58
# Parent  c07187514ce5fc51d464acd68bf4f1bf275e5b0e
*** empty log message ***

diff -r c07187514ce5 -r a1bb7a7b6205 doc-src/HOL/logics-HOL.bbl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/HOL/logics-HOL.bbl	Tue May 04 19:08:58 1999 +0200
@@ -0,0 +1,202 @@
+\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.
+
+\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.
+
+\bibitem{frost93}
+Jacob Frost.
+\newblock A case study of co-induction in {Isabelle HOL}.
+\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.
+
+\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}
+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.
+
+\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.
+
+\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.
+
+\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.
+\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12
+  International Conference}, LNAI 814, pages 148--161. Springer, 1994.
+
+\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.
+
+\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.
+
+\bibitem{paulson-security}
+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.
+
+\bibitem{paulson-COLOG}
+Lawrence~C. Paulson.
+\newblock A formulation of the simple theory of types (for {Isabelle}).
+\newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
+  International Conference on Computer Logic}, LNCS 417, pages 246--274,
+  Tallinn, Published 1990. Estonian Academy of Sciences, Springer.
+
+\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 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.
+
+\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.
+
+\bibitem{winskel93}
+Glynn Winskel.
+\newblock {\em The Formal Semantics of Programming Languages}.
+\newblock MIT Press, 1993.
+
+\end{thebibliography}