# HG changeset patch # User paulson # Date 925915482 -7200 # Node ID c120262044b6b7e2ff2a880f76b2a2f4b23f8b1c # Parent 6a753a6d6738012b684288aca7d8133a54316ed2 Now uses manual.bib; some references updated diff -r 6a753a6d6738 -r c120262044b6 doc-src/HOL/HOL.tex --- a/doc-src/HOL/HOL.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/HOL/HOL.tex Wed May 05 16:44:42 1999 +0200 @@ -1547,7 +1547,7 @@ slightly more advanced, though, supporting \emph{extensible record schemes}. This admits operations that are polymorphic with respect to record extension, yielding ``object-oriented'' effects like (single) inheritance. See also -\cite{Naraschewski-Wenzel:1998:TPHOL} for more details on object-oriented +\cite{NaraschewskiW-TPHOLs98} for more details on object-oriented verification and record subtyping in HOL. @@ -2763,12 +2763,12 @@ \section{The examples directories} -Directory \texttt{HOL/Auth} contains theories for proving the correctness of -cryptographic protocols. The approach is based upon operational -semantics~\cite{paulson-security} rather than the more usual belief logics. -On the same directory are proofs for some standard examples, such as the -Needham-Schroeder public-key authentication protocol~\cite{paulson-ns} -and the Otway-Rees protocol. +Directory \texttt{HOL/Auth} contains theories for proving the correctness of +cryptographic protocols~\cite{paulson-jcs}. The approach is based upon +operational semantics rather than the more usual belief logics. On the same +directory are proofs for some standard examples, such as the Needham-Schroeder +public-key authentication protocol and the Otway-Rees +protocol. Directory \texttt{HOL/IMP} contains a formalization of various denotational, operational and axiomatic semantics of a simple while-language, the necessary diff -r 6a753a6d6738 -r c120262044b6 doc-src/HOL/logics-HOL.bbl --- 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. diff -r 6a753a6d6738 -r c120262044b6 doc-src/HOL/logics-HOL.tex --- a/doc-src/HOL/logics-HOL.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/HOL/logics-HOL.tex Wed May 05 16:44:42 1999 +0200 @@ -56,7 +56,6 @@ \include{../Logics/syntax} \include{HOL} \bibliographystyle{plain} -\bibliography{../isabelle} -%\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref} +\bibliography{../manual} \input{logics-HOL.ind} \end{document} diff -r 6a753a6d6738 -r c120262044b6 doc-src/Intro/foundations.tex --- a/doc-src/Intro/foundations.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Intro/foundations.tex Wed May 05 16:44:42 1999 +0200 @@ -959,7 +959,7 @@ rather than on individual subgoals. An Isabelle tactic is a function that takes a proof state and returns a sequence (lazy list) of possible successor states. Lazy lists are coded in ML as functions, a standard -technique~\cite{paulson91}. Isabelle represents proof states by theorems. +technique~\cite{paulson-ml2}. Isabelle represents proof states by theorems. Basic tactics execute the meta-rules described above, operating on a given subgoal. The {\bf resolution tactics} take a list of rules and diff -r 6a753a6d6738 -r c120262044b6 doc-src/Intro/intro.bbl --- a/doc-src/Intro/intro.bbl Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Intro/intro.bbl Wed May 05 16:44:42 1999 +0200 @@ -69,11 +69,6 @@ \newblock In P.~Odifreddi, editor, {\em Logic and Computer Science}, pages 361--386. Academic Press, 1990. -\bibitem{paulson91} -Lawrence~C. Paulson. -\newblock {\em {ML} for the Working Programmer}. -\newblock Cambridge University Press, 1991. - \bibitem{paulson-handbook} Lawrence~C. Paulson. \newblock Designing a theorem prover. @@ -81,6 +76,11 @@ Handbook of Logic in Computer Science}, volume~2, pages 415--475. Oxford University Press, 1992. +\bibitem{paulson-ml2} +Lawrence~C. Paulson. +\newblock {\em {ML} for the Working Programmer}. +\newblock Cambridge University Press, 2nd edition, 1996. + \bibitem{pelletier86} F.~J. Pelletier. \newblock Seventy-five problems for testing automatic theorem provers. diff -r 6a753a6d6738 -r c120262044b6 doc-src/Intro/intro.tex --- a/doc-src/Intro/intro.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Intro/intro.tex Wed May 05 16:44:42 1999 +0200 @@ -64,7 +64,7 @@ knowledge of Standard~\ML{} is essential, because \ML{} is Isabelle's user interface. Advanced Isabelle theorem proving can involve writing \ML{} code, possibly with Isabelle's sources at hand. My book -on~\ML{}~\cite{paulson91} covers much material connected with Isabelle, +on~\ML{}~\cite{paulson-ml2} covers much material connected with Isabelle, including a simple theorem prover. Users must be familiar with logic as used in computer science; there are many good texts~\cite{galton90,reeves90}. @@ -135,7 +135,7 @@ \include{advanced} \bibliographystyle{plain} \small\raggedright\frenchspacing -\bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref} +\bibliography{../manual} \input{intro.ind} \end{document} diff -r 6a753a6d6738 -r c120262044b6 doc-src/Logics/logics.bbl --- a/doc-src/Logics/logics.bbl Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Logics/logics.bbl Wed May 05 16:44:42 1999 +0200 @@ -1,16 +1,5 @@ \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}. @@ -30,24 +19,12 @@ \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 @@ -61,124 +38,32 @@ 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}. @@ -189,14 +74,4 @@ \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} diff -r 6a753a6d6738 -r c120262044b6 doc-src/Logics/logics.tex --- a/doc-src/Logics/logics.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Logics/logics.tex Wed May 05 16:44:42 1999 +0200 @@ -53,6 +53,6 @@ %%\include{Cube} %%\include{LCF} \bibliographystyle{plain} -\bibliography{bib,string,general,atp,theory,funprog,logicprog,isabelle,crossref} +\bibliography{../manual} \input{logics.ind} \end{document} diff -r 6a753a6d6738 -r c120262044b6 doc-src/Ref/classical.tex --- a/doc-src/Ref/classical.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Ref/classical.tex Wed May 05 16:44:42 1999 +0200 @@ -112,7 +112,7 @@ theorem and apply rules backwards in a fairly arbitrary manner. This yields a surprisingly effective proof procedure. Quantifiers add few complications, since Isabelle handles parameters and schematic variables. See Chapter~10 -of {\em ML for the Working Programmer}~\cite{paulson91} for further +of {\em ML for the Working Programmer}~\cite{paulson-ml2} for further discussion. diff -r 6a753a6d6738 -r c120262044b6 doc-src/Ref/defining.tex --- a/doc-src/Ref/defining.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Ref/defining.tex Wed May 05 16:44:42 1999 +0200 @@ -584,7 +584,7 @@ space and followed by a space or line break; the entire phrase is a pretty printing block. Other examples appear in Fig.\ts\ref{fig:set_trans} below. Isabelle's pretty printer resembles the one described in -Paulson~\cite{paulson91}. +Paulson~\cite{paulson-ml2}. \index{pretty printing|)} diff -r 6a753a6d6738 -r c120262044b6 doc-src/Ref/ref.bbl --- a/doc-src/Ref/ref.bbl Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Ref/ref.bbl Wed May 05 16:44:42 1999 +0200 @@ -44,11 +44,6 @@ \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}. \newblock Oxford University Press, 1990. -\bibitem{paulson91} -Lawrence~C. Paulson. -\newblock {\em {ML} for the Working Programmer}. -\newblock Cambridge University Press, 1991. - \bibitem{paulson-ml2} Lawrence~C. Paulson. \newblock {\em {ML} for the Working Programmer}. diff -r 6a753a6d6738 -r c120262044b6 doc-src/Ref/ref.tex --- a/doc-src/Ref/ref.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Ref/ref.tex Wed May 05 16:44:42 1999 +0200 @@ -63,7 +63,7 @@ \begingroup \bibliographystyle{plain} \small\raggedright\frenchspacing - \bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref} + \bibliography{../manual} \endgroup \include{theory-syntax} diff -r 6a753a6d6738 -r c120262044b6 doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Ref/theories.tex Wed May 05 16:44:42 1999 +0200 @@ -486,7 +486,7 @@ number of lambdas, starting from zero, between a variable's occurrence and its binding. The representation prevents capture of variables. For more information see de Bruijn \cite{debruijn72} or - Paulson~\cite[page~336]{paulson91}. + Paulson~\cite[page~376]{paulson-ml2}. \item[\ttindexbold{Abs} ($a$, $T$, $u$)] \index{lambda abs@$\lambda$-abstractions|bold} diff -r 6a753a6d6738 -r c120262044b6 doc-src/ZF/ZF.tex --- a/doc-src/ZF/ZF.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/ZF/ZF.tex Wed May 05 16:44:42 1999 +0200 @@ -31,7 +31,7 @@ Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF} less formally than this chapter. Isabelle employs a novel treatment of non-well-founded data structures within the standard {\sc zf} axioms including -the Axiom of Foundation~\cite{paulson-final}. +the Axiom of Foundation~\cite{paulson-mscs}. \section{Which version of axiomatic set theory?} @@ -1116,7 +1116,7 @@ non-standard notion of disjoint sum using non-standard pairs. All of these concepts satisfy the same properties as their standard counterparts; in addition, {\tt<$a$;$b$>} is continuous. The theory supports coinductive -definitions, for example of infinite lists~\cite{paulson-final}. +definitions, for example of infinite lists~\cite{paulson-mscs}. \begin{figure} \begin{ttbox} @@ -2386,10 +2386,10 @@ induction. \item Theory \texttt{ListN} inductively defines the lists of $n$ - elements~\cite{paulin92}. + elements~\cite{paulin-tlca}. \item Theory \texttt{Acc} inductively defines the accessible part of a - relation~\cite{paulin92}. + relation~\cite{paulin-tlca}. \item Theory \texttt{Comb} defines the datatype of combinators and inductively defines contraction and parallel contraction. It goes on to diff -r 6a753a6d6738 -r c120262044b6 doc-src/ZF/logics-ZF.bbl --- a/doc-src/ZF/logics-ZF.bbl Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/ZF/logics-ZF.bbl Wed May 05 16:44:42 1999 +0200 @@ -16,7 +16,7 @@ Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and Lawrence Wos. \newblock Set theory in first-order logic: Clauses for {G\"{o}del's} axioms. -\newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986. +\newblock {\em J. Auto. Reas.}, 2(3):287--327, 1986. \bibitem{camilleri92} J.~Camilleri and T.~F. Melham. @@ -43,7 +43,7 @@ \bibitem{dyckhoff} Roy Dyckhoff. \newblock Contraction-free sequent calculi for intuitionistic logic. -\newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992. +\newblock {\em J. Symb. Logic}, 57(3):795--807, 1992. \bibitem{halmos60} Paul~R. Halmos. @@ -58,13 +58,13 @@ \bibitem{noel} Philippe No{\"e}l. \newblock Experimenting with {Isabelle} in {ZF} set theory. -\newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993. +\newblock {\em J. Auto. Reas.}, 10(1):15--58, 1993. -\bibitem{paulin92} +\bibitem{paulin-tlca} 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. +\newblock In M.~Bezem and J.F. Groote, editors, {\em Typed Lambda Calculi and + Applications}, LNCS 664, pages 328--345. Springer, 1993. \bibitem{paulson87} Lawrence~C. Paulson. @@ -74,7 +74,7 @@ \bibitem{paulson-set-I} Lawrence~C. Paulson. \newblock Set theory for verification: {I}. {From} foundations to functions. -\newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993. +\newblock {\em J. Auto. Reas.}, 11(3):353--389, 1993. \bibitem{paulson-CADE} Lawrence~C. Paulson. @@ -82,17 +82,10 @@ \newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12 International Conference}, LNAI 814, pages 148--161. Springer, 1994. -\bibitem{paulson-final} -Lawrence~C. Paulson. -\newblock A concrete final coalgebra theorem for {ZF} set theory. -\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em - Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996, - pages 120--139. Springer, 1995. - \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. +\newblock {\em J. Auto. Reas.}, 15(2):167--215, 1995. \bibitem{paulson-generic} Lawrence~C. Paulson. @@ -100,10 +93,16 @@ \newblock In Robert Veroff, editor, {\em Automated Reasoning and its Applications: Essays in Honor of {Larry Wos}}, chapter~3. MIT Press, 1997. +\bibitem{paulson-mscs} +Lawrence~C. Paulson. +\newblock Final coalgebras as greatest fixed points in zf set theory. +\newblock {\em Mathematical Structures in Computer Science}, 9, 1999. +\newblock in press. + \bibitem{quaife92} Art Quaife. \newblock Automated deduction in {von Neumann-Bernays-G\"{o}del} set theory. -\newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992. +\newblock {\em J. Auto. Reas.}, 8(1):91--147, 1992. \bibitem{suppes72} Patrick Suppes. diff -r 6a753a6d6738 -r c120262044b6 doc-src/ZF/logics-ZF.tex --- a/doc-src/ZF/logics-ZF.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/ZF/logics-ZF.tex Wed May 05 16:44:42 1999 +0200 @@ -57,6 +57,6 @@ \include{FOL} \include{ZF} \bibliographystyle{plain} -\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref} +\bibliography{../manual} \input{logics-ZF.ind} \end{document} diff -r 6a753a6d6738 -r c120262044b6 doc-src/isabelle.bib --- a/doc-src/isabelle.bib Wed May 05 14:31:31 1999 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,58 +0,0 @@ -@string{AP="Academic Press"} -@string{CUP="Cambridge University Press"} -@string{FAC="Formal Aspects of Computing"} -@string{JSL="J. Symbolic Logic"} -@string{LNCS="Lect.\ Notes in Comp.\ Sci."} -@string{MIT="MIT Press"} -@string{Springer="Springer-Verlag"} - -@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} - -@book{mgordon-hol,editor="M.J.C. Gordon and T.F. Melham", -title= -"Introduction to {HOL}: a theorem-proving environment for higher order logic", -publisher=CUP,year=1993} - -@article{church40,author="Alonzo Church", -title="A Formulation of the Simple Theory of Types", -journal=JSL,year=1940,volume=5,pages="56--68"} - -@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"} - -@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{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} - -@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} - -@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{winskel93,author={Glynn Winskel}, -title={The Formal Semantics of Programming Languages},publisher=MIT,year=1993} diff -r 6a753a6d6738 -r c120262044b6 doc-src/manual.bib --- /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}