--- a/doc-src/Logics/logics.bbl Thu Nov 11 13:24:47 1993 +0100
+++ b/doc-src/Logics/logics.bbl Fri Nov 12 10:41:13 1993 +0100
@@ -6,11 +6,24 @@
Through Proof}.
\newblock Academic Press, 1986.
+\bibitem{basin91}
+David Basin and Matt Kaufmann.
+\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison.
+\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
+ Frameworks}, pages 89--119. Cambridge University Press, 1991.
+
\bibitem{boyer86}
Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and
Lawrence Wos.
\newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms.
-\newblock {\em Journal of Automated Reasoning}, 2:287--327, 1986.
+\newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986.
+
+\bibitem{camilleri92}
+J.~Camilleri and T.~F. Melham.
+\newblock Reasoning with inductively defined relations in the {HOL} theorem
+ prover.
+\newblock Technical Report 265, University of Cambridge Computer Laboratory,
+ August 1992.
\bibitem{church40}
Alonzo Church.
@@ -20,7 +33,7 @@
\bibitem{dummett}
Michael Dummett.
\newblock {\em Elements of Intuitionism}.
-\newblock Oxford, 1977.
+\newblock Oxford University Press, 1977.
\bibitem{dyckhoff}
Roy Dyckhoff.
@@ -35,6 +48,12 @@
Programming}, pages 157--178. Springer, 1991.
\newblock LNAI 475.
+\bibitem{frost93}
+Jacob Frost.
+\newblock A case study of co-induction in {Isabelle HOL}.
+\newblock Technical Report 308, University of Cambridge Computer Laboratory,
+ August 1993.
+
\bibitem{OBJ}
K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer.
\newblock Principles of {OBJ2}.
@@ -47,7 +66,7 @@
Proving}.
\newblock Harper \& Row, 1986.
-\bibitem{gordon88a}
+\bibitem{mgordon88a}
Michael J.~C. Gordon.
\newblock {HOL}: A proof generating system for higher-order logic.
\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em {VLSI}
@@ -65,27 +84,48 @@
second-order patterns.
\newblock {\em Acta Informatica}, 11:31--55, 1978.
+\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{nipkow-prehofer}
-Tobias Nipkow and Christian Prehofer.
-\newblock Type checking type classes.
-\newblock In {\em 20th ACM Symp.\ Principles of Programming Languages}, 1993.
-\newblock To appear.
+\bibitem{milner-coind}
+Robin Milner and Mads Tofte.
+\newblock Co-induction in relational semantics.
+\newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
\bibitem{noel}
Philippe {No\"el}.
\newblock Experimenting with {Isabelle} in {ZF} set theory.
-\newblock {\em Journal of Automated Reasoning}.
-\newblock In press.
+\newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993.
\bibitem{nordstrom90}
Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
-\newblock Oxford, 1990.
+\newblock Oxford University Press, 1990.
+
+\bibitem{paulin92}
+Christine Paulin-Mohring.
+\newblock Inductive definitions in the system {Coq}: Rules and properties.
+\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
+ December 1992.
+
+\bibitem{paulson-set-I}
+Lawrence~C. Paulson.
+\newblock Set theory for verification: {I}. {From} foundations to functions.
+\newblock {\em Journal of Automated Reasoning}.
+\newblock In press; draft available as Report 271, University of Cambridge
+ Computer Laboratory.
+
+\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.
@@ -100,6 +140,29 @@
of Sciences, Springer.
\newblock LNCS 417.
+\bibitem{paulson91}
+Lawrence~C. Paulson.
+\newblock {\em {ML} for the Working Programmer}.
+\newblock Cambridge University Press, 1991.
+
+\bibitem{paulson-coind}
+Lawrence~C. Paulson.
+\newblock Co-induction and co-recursion in higher-order logic.
+\newblock Technical Report 304, University of Cambridge Computer Laboratory,
+ July 1993.
+
+\bibitem{paulson-fixedpt}
+Lawrence~C. Paulson.
+\newblock A fixedpoint approach to implementing (co-)inductive definitions.
+\newblock Technical report, University of Cambridge Computer Laboratory, 1993.
+\newblock Draft.
+
+\bibitem{paulson-set-II}
+Lawrence~C. Paulson.
+\newblock Set theory for verification: {II}. {Induction} and recursion.
+\newblock Technical Report 312, University of Cambridge Computer Laboratory,
+ 1993.
+
\bibitem{pelletier86}
F.~J. Pelletier.
\newblock Seventy-five problems for testing automatic theorem provers.