1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/HOL/logics-HOL.bbl	Tue May 04 19:08:58 1999 +0200
     1.3 @@ -0,0 +1,202 @@
     1.4 +\begin{thebibliography}{10}
     1.5 +
     1.6 +\bibitem{andrews86}
     1.7 +Peter~B. Andrews.
     1.8 +\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
     1.9 +  Through Proof}.
    1.10 +\newblock Academic Press, 1986.
    1.11 +
    1.12 +\bibitem{church40}
    1.13 +Alonzo Church.
    1.14 +\newblock A formulation of the simple theory of types.
    1.15 +\newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.
    1.16 +
    1.17 +\bibitem{coen92}
    1.18 +Martin~D. Coen.
    1.19 +\newblock {\em Interactive Program Derivation}.
    1.20 +\newblock PhD thesis, University of Cambridge, November 1992.
    1.21 +\newblock Computer Laboratory Technical Report 272.
    1.22 +
    1.23 +\bibitem{constable86}
    1.24 +R.~L. Constable et~al.
    1.25 +\newblock {\em Implementing Mathematics with the Nuprl Proof Development
    1.26 +  System}.
    1.27 +\newblock Prentice-Hall, 1986.
    1.28 +
    1.29 +\bibitem{felty91a}
    1.30 +Amy Felty.
    1.31 +\newblock A logic program for transforming sequent proofs to natural deduction
    1.32 +  proofs.
    1.33 +\newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic
    1.34 +  Programming}, LNAI 475, pages 157--178. Springer, 1991.
    1.35 +
    1.36 +\bibitem{frost93}
    1.37 +Jacob Frost.
    1.38 +\newblock A case study of co-induction in {Isabelle HOL}.
    1.39 +\newblock Technical Report 308, Computer Laboratory, University of Cambridge,
    1.40 +  August 1993.
    1.41 +
    1.42 +\bibitem{gallier86}
    1.43 +J.~H. Gallier.
    1.44 +\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
    1.45 +  Proving}.
    1.46 +\newblock Harper \& Row, 1986.
    1.47 +
    1.48 +\bibitem{mgordon-hol}
    1.49 +M.~J.~C. Gordon and T.~F. Melham.
    1.50 +\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
    1.51 +  Order Logic}.
    1.52 +\newblock Cambridge University Press, 1993.
    1.53 +
    1.54 +\bibitem{huet78}
    1.55 +G.~P. Huet and B.~Lang.
    1.56 +\newblock Proving and applying program transformations expressed with
    1.57 +  second-order patterns.
    1.58 +\newblock {\em Acta Informatica}, 11:31--55, 1978.
    1.59 +
    1.60 +\bibitem{alf}
    1.61 +Lena Magnusson and Bengt {Nordstr\"{o}m}.
    1.62 +\newblock The {ALF} proof editor and its proof engine.
    1.63 +\newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs
    1.64 +  and Programs: International Workshop {TYPES '93}}, LNCS 806, pages 213--237.
    1.65 +  Springer, published 1994.
    1.66 +
    1.67 +\bibitem{mw81}
    1.68 +Zohar Manna and Richard Waldinger.
    1.69 +\newblock Deductive synthesis of the unification algorithm.
    1.70 +\newblock {\em Science of Computer Programming}, 1(1):5--48, 1981.
    1.71 +
    1.72 +\bibitem{martinlof84}
    1.73 +Per Martin-L\"of.
    1.74 +\newblock {\em Intuitionistic type theory}.
    1.75 +\newblock Bibliopolis, 1984.
    1.76 +
    1.77 +\bibitem{milner78}
    1.78 +Robin Milner.
    1.79 +\newblock A theory of type polymorphism in programming.
    1.80 +\newblock {\em Journal of Computer and System Sciences}, 17:348--375, 1978.
    1.81 +
    1.82 +\bibitem{milner-coind}
    1.83 +Robin Milner and Mads Tofte.
    1.84 +\newblock Co-induction in relational semantics.
    1.85 +\newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
    1.86 +
    1.87 +\bibitem{Naraschewski-Wenzel:1998:TPHOL}
    1.88 +Wolfgang Naraschewski and Markus Wenzel.
    1.89 +\newblock Object-oriented verification based on record subtyping in
    1.90 +  higher-order logic.
    1.91 +\newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in
    1.92 +  Higher Order Logics: {TPHOLs} '98}, LNCS 1479, pages 349--366, 1998.
    1.93 +
    1.94 +\bibitem{nazareth-nipkow}
    1.95 +Dieter Nazareth and Tobias Nipkow.
    1.96 +\newblock Formal verification of algorithm {W}: The monomorphic case.
    1.97 +\newblock In von Wright et~al. \cite{tphols96}, pages 331--345.
    1.98 +
    1.99 +\bibitem{Nipkow-CR}
   1.100 +Tobias Nipkow.
   1.101 +\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}).
   1.102 +\newblock In Michael McRobbie and John~K. Slaney, editors, {\em Automated
   1.103 +  Deduction --- {CADE}-13 International Conference}, LNAI 1104, pages 733--747.
   1.104 +  Springer, 1996.
   1.105 +
   1.106 +\bibitem{nipkow-IMP}
   1.107 +Tobias Nipkow.
   1.108 +\newblock Winskel is (almost) right: Towards a mechanized semantics textbook.
   1.109 +\newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software
   1.110 +  Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS},
   1.111 +  pages 180--192. Springer, 1996.
   1.112 +
   1.113 +\bibitem{nordstrom90}
   1.114 +Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
   1.115 +\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
   1.116 +\newblock Oxford University Press, 1990.
   1.117 +
   1.118 +\bibitem{paulson85}
   1.119 +Lawrence~C. Paulson.
   1.120 +\newblock Verifying the unification algorithm in {LCF}.
   1.121 +\newblock {\em Science of Computer Programming}, 5:143--170, 1985.
   1.122 +
   1.123 +\bibitem{paulson87}
   1.124 +Lawrence~C. Paulson.
   1.125 +\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
   1.126 +\newblock Cambridge University Press, 1987.
   1.127 +
   1.128 +\bibitem{paulson-CADE}
   1.129 +Lawrence~C. Paulson.
   1.130 +\newblock A fixedpoint approach to implementing (co)inductive definitions.
   1.131 +\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12
   1.132 +  International Conference}, LNAI 814, pages 148--161. Springer, 1994.
   1.133 +
   1.134 +\bibitem{paulson-set-II}
   1.135 +Lawrence~C. Paulson.
   1.136 +\newblock Set theory for verification: {II}. {Induction} and recursion.
   1.137 +\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
   1.138 +
   1.139 +\bibitem{paulson-ns}
   1.140 +Lawrence~C. Paulson.
   1.141 +\newblock Mechanized proofs of security protocols: {Needham-Schroeder} with
   1.142 +  public keys.
   1.143 +\newblock Technical Report 413, Computer Laboratory, University of Cambridge,
   1.144 +  January 1997.
   1.145 +
   1.146 +\bibitem{paulson-coind}
   1.147 +Lawrence~C. Paulson.
   1.148 +\newblock Mechanizing coinduction and corecursion in higher-order logic.
   1.149 +\newblock {\em Journal of Logic and Computation}, 7(2):175--204, March 1997.
   1.150 +
   1.151 +\bibitem{paulson-security}
   1.152 +Lawrence~C. Paulson.
   1.153 +\newblock Proving properties of security protocols by induction.
   1.154 +\newblock In {\em 10th Computer Security Foundations Workshop}, pages 70--83.
   1.155 +  IEEE Computer Society Press, 1997.
   1.156 +
   1.157 +\bibitem{isabelle-ZF}
   1.158 +Lawrence~C. Paulson.
   1.159 +\newblock {Isabelle}'s logics: {FOL} and {ZF}.
   1.160 +\newblock Technical report, Computer Laboratory, University of Cambridge, 1999.
   1.161 +
   1.162 +\bibitem{paulson-COLOG}
   1.163 +Lawrence~C. Paulson.
   1.164 +\newblock A formulation of the simple theory of types (for {Isabelle}).
   1.165 +\newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
   1.166 +  International Conference on Computer Logic}, LNCS 417, pages 246--274,
   1.167 +  Tallinn, Published 1990. Estonian Academy of Sciences, Springer.
   1.168 +
   1.169 +\bibitem{pelletier86}
   1.170 +F.~J. Pelletier.
   1.171 +\newblock Seventy-five problems for testing automatic theorem provers.
   1.172 +\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
   1.173 +\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
   1.174 +
   1.175 +\bibitem{plaisted90}
   1.176 +David~A. Plaisted.
   1.177 +\newblock A sequent-style model elimination strategy and a positive refinement.
   1.178 +\newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990.
   1.179 +
   1.180 +\bibitem{slind-tfl}
   1.181 +Konrad Slind.
   1.182 +\newblock Function definition in higher-order logic.
   1.183 +\newblock In von Wright et~al. \cite{tphols96}.
   1.184 +
   1.185 +\bibitem{takeuti87}
   1.186 +G.~Takeuti.
   1.187 +\newblock {\em Proof Theory}.
   1.188 +\newblock North-Holland, 2nd edition, 1987.
   1.189 +
   1.190 +\bibitem{thompson91}
   1.191 +Simon Thompson.
   1.192 +\newblock {\em Type Theory and Functional Programming}.
   1.193 +\newblock Addison-Wesley, 1991.
   1.194 +
   1.195 +\bibitem{tphols96}
   1.196 +J.~von Wright, J.~Grundy, and J.~Harrison, editors.
   1.197 +\newblock {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96}, LNCS
   1.198 +  1125, 1996.
   1.199 +
   1.200 +\bibitem{winskel93}
   1.201 +Glynn Winskel.
   1.202 +\newblock {\em The Formal Semantics of Programming Languages}.
   1.203 +\newblock MIT Press, 1993.
   1.204 +
   1.205 +\end{thebibliography}