doc-src/springer.bbl

+\begin{thebibliography}{10}
+
+\bibitem{andrews86}
+Andrews, P.~B.,
+\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
+  Through Proof},
+\newblock Academic Press, 1986
+
+\bibitem{basin91}
+Basin, D., Kaufmann, M.,
+\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison,
+\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge
+  Univ. Press, 1991, pp.~89--119
+
+\bibitem{boyer86}
+Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.,
+\newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms,
+\newblock {\em J. Auto. Reas. {\bf 2}}, 3 (1986), 287--327
+
+\bibitem{bm88book}
+Boyer, R.~S., Moore, J.~S.,
+\newblock {\em A Computational Logic Handbook},
+\newblock Academic Press, 1988
+
+\bibitem{camilleri92}
+Camilleri, J., Melham, T.~F.,
+\newblock Reasoning with inductively defined relations in the {HOL} theorem
+  prover,
+\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
+
+\bibitem{charniak80}
+Charniak, E., Riesbeck, C.~K., McDermott, D.~V.,
+\newblock {\em Artificial Intelligence Programming},
+\newblock Lawrence Erlbaum Associates, 1980
+
+\bibitem{church40}
+Church, A.,
+\newblock A formulation of the simple theory of types,
+\newblock {\em J. Symb. Logic {\bf 5}\/} (1940), 56--68
+
+\bibitem{coen92}
+Coen, M.~D.,
+\newblock {\em Interactive Program Derivation},
+\newblock PhD thesis, University of Cambridge, 1992,
+\newblock Computer Laboratory Technical Report 272
+
+\bibitem{constable86}
+{Constable et al.}, R.~L.,
+\newblock {\em Implementing Mathematics with the Nuprl Proof Development
+  System},
+\newblock Prentice-Hall, 1986
+
+\bibitem{davey&priestley}
+Davey, B.~A., Priestley, H.~A.,
+\newblock {\em Introduction to Lattices and Order},
+\newblock Cambridge Univ. Press, 1990
+
+\bibitem{dawson90}
+Dawson, W.~M.,
+\newblock {\em A Generic Logic Environment},
+\newblock PhD thesis, Imperial College, London, 1990
+
+\bibitem{debruijn72}
+de~Bruijn, N.~G.,
+\newblock Lambda calculus notation with nameless dummies, a tool for automatic
+  formula manipulation, with application to the {Church-Rosser Theorem},
+\newblock {\em Indag. Math. {\bf 34}\/} (1972), 381--392
+
+\bibitem{devlin79}
+Devlin, K.~J.,
+\newblock {\em Fundamentals of Contemporary Set Theory},
+\newblock Springer, 1979
+
+\bibitem{coq}
+{Dowek et al.}, G.,
+\newblock The {Coq} proof assistant user's guide,
+\newblock Technical Report 134, INRIA-Rocquencourt, 1991
+
+\bibitem{dummett}
+Dummett, M.,
+\newblock {\em Elements of Intuitionism},
+\newblock Oxford University Press, 1977
+
+\bibitem{dyckhoff}
+Dyckhoff, R.,
+\newblock Contraction-free sequent calculi for intuitionistic logic,
+\newblock {\em J. Symb. Logic {\bf 57}}, 3 (1992), 795--807
+
+\bibitem{felty91a}
+Felty, A.,
+\newblock A logic program for transforming sequent proofs to natural deduction
+  proofs,
+\newblock In {\em Extensions of Logic Programming\/} (1991),
+  P.~Schroeder-Heister, Ed., Springer, pp.~157--178,
+\newblock LNAI 475
+
+\bibitem{felty93}
+Felty, A.,
+\newblock Implementing tactics and tacticals in a higher-order logic
+  programming language,
+\newblock {\em J. Auto. Reas. {\bf 11}}, 1 (1993), 43--82
+
+\bibitem{frost93}
+Frost, J.,
+\newblock A case study of co-induction in {Isabelle HOL},
+\newblock Tech. Rep. 308, Comp. Lab., Univ. Cambridge, Aug. 1993
+
+\bibitem{OBJ}
+Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.,
+\newblock Principles of {OBJ2},
+\newblock In {\em Princ. Prog. Lang.\/} (1985), pp.~52--66
+
+\bibitem{gallier86}
+Gallier, J.~H.,
+\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
+  Proving},
+\newblock Harper \& Row, 1986
+
+\bibitem{mgordon-hol}
+Gordon, M. J.~C., Melham, T.~F.,
+\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
+  Order Logic},
+\newblock Cambridge Univ. Press, 1993
+
+\bibitem{halmos60}
+Halmos, P.~R.,
+\newblock {\em Naive Set Theory},
+\newblock Van Nostrand, 1960
+
+\bibitem{harper-jacm}
+Harper, R., Honsell, F., Plotkin, G.,
+\newblock A framework for defining logics,
+\newblock {\em J.~ACM {\bf 40}}, 1 (1993), 143--184
+
+\bibitem{haskell-tutorial}
+Hudak, P., Fasel, J.~H.,
+\newblock A gentle introduction to {Haskell},
+\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992)
+
+\bibitem{haskell-report}
+Hudak, P., Jones, S.~P., Wadler, P.,
+\newblock Report on the programming language {Haskell}: A non-strict, purely
+  functional language,
+\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992),
+\newblock Version 1.2
+
+\bibitem{huet75}
+Huet, G.~P.,
+\newblock A unification algorithm for typed $\lambda$-calculus,
+\newblock {\em Theoretical Comput. Sci. {\bf 1}\/} (1975), 27--57
+
+\bibitem{huet78}
+Huet, G.~P., Lang, B.,
+\newblock Proving and applying program transformations expressed with
+  second-order patterns,
+\newblock {\em Acta Inf. {\bf 11}\/} (1978), 31--55
+
+\bibitem{mural}
+Jones, C.~B., Jones, K.~D., Lindsay, P.~A., Moore, R.,
+\newblock {\em Mural: A Formal Development Support System},
+\newblock Springer, 1991
+
+\bibitem{alf}
+Magnusson, L., {Nordstr\"om}, B.,
+\newblock The {ALF} proof editor and its proof engine,
+\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
+  '93}\/} (published 1994), Springer, pp.~213--237,
+\newblock LNCS 806
+
+\bibitem{mw81}
+Manna, Z., Waldinger, R.,
+\newblock Deductive synthesis of the unification algorithm,
+\newblock {\em Sci. Comput. Programming {\bf 1}}, 1 (1981), 5--48
+
+\bibitem{martin-nipkow}
+Martin, U., Nipkow, T.,
+\newblock Ordered rewriting and confluence,
+\newblock In {\em 10th Conf. Auto. Deduct.\/} (1990), M.~E. Stickel, Ed.,
+  Springer, pp.~366--380,
+\newblock LNCS 449
+
+\bibitem{martinlof84}
+Martin-L\"of, P.,
+\newblock {\em Intuitionistic type theory},
+\newblock Bibliopolis, 1984
+
+\bibitem{melham89}
+Melham, T.~F.,
+\newblock Automating recursive type definitions in higher order logic,
+\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
+  Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,
+  pp.~341--386
+
+\bibitem{miller-mixed}
+Miller, D.,
+\newblock Unification under a mixed prefix,
+\newblock {\em J. Symb. Comput. {\bf 14}}, 4 (1992), 321--358
+
+\bibitem{milner-coind}
+Milner, R., Tofte, M.,
+\newblock Co-induction in relational semantics,
+\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
+
+\bibitem{nipkow-prehofer}
+Nipkow, T., Prehofer, C.,
+\newblock Type checking type classes,
+\newblock In {\em 20th Princ. Prog. Lang.\/} (1993), ACM Press, pp.~409--418,
+\newblock Revised version to appear in \bgroup\em J. Func. Prog.\egroup
+
+\bibitem{noel}
+{No\"el}, P.,
+\newblock Experimenting with {Isabelle} in {ZF} set theory,
+\newblock {\em J. Auto. Reas. {\bf 10}}, 1 (1993), 15--58
+
+\bibitem{nordstrom90}
+{Nordstr\"om}, B., Petersson, K., Smith, J.,
+\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction},
+\newblock Oxford University Press, 1990
+
+\bibitem{paulin92}
+Paulin-Mohring, C.,
+\newblock Inductive definitions in the system {Coq}: Rules and properties,
+\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.
+  1992
+
+\bibitem{paulson85}
+Paulson, L.~C.,
+\newblock Verifying the unification algorithm in {LCF},
+\newblock {\em Sci. Comput. Programming {\bf 5}\/} (1985), 143--170
+
+\bibitem{paulson87}
+Paulson, L.~C.,
+\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
+\newblock Cambridge Univ. Press, 1987
+
+\bibitem{paulson89}
+Paulson, L.~C.,
+\newblock The foundation of a generic theorem prover,
+\newblock {\em J. Auto. Reas. {\bf 5}}, 3 (1989), 363--397
+
+\bibitem{paulson-COLOG}
+Paulson, L.~C.,
+\newblock A formulation of the simple theory of types (for {Isabelle}),
+\newblock In {\em COLOG-88: International Conference on Computer Logic\/}
+  (Tallinn, 1990), P.~Martin-L\"of, G.~Mints, Eds., Estonian Academy of
+  Sciences, Springer,
+\newblock LNCS 417
+
+\bibitem{paulson700}
+Paulson, L.~C.,
+\newblock {Isabelle}: The next 700 theorem provers,
+\newblock In {\em Logic and Computer Science}, P.~Odifreddi, Ed. Academic
+  Press, 1990, pp.~361--386
+
+\bibitem{paulson91}
+Paulson, L.~C.,
+\newblock {\em {ML} for the Working Programmer},
+\newblock Cambridge Univ. Press, 1991
+
+\bibitem{paulson-coind}
+Paulson, L.~C.,
+\newblock Co-induction and co-recursion in higher-order logic,
+\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
+
+\bibitem{paulson-fixedpt}
+Paulson, L.~C.,
+\newblock A fixedpoint approach to implementing (co)inductive definitions,
+\newblock Tech. Rep. 320, Comp. Lab., Univ. Cambridge, Dec. 1993
+
+\bibitem{paulson-set-I}
+Paulson, L.~C.,
+\newblock Set theory for verification: {I}. {From} foundations to functions,
+\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
+
+\bibitem{paulson-set-II}
+Paulson, L.~C.,
+\newblock Set theory for verification: {II}. {Induction} and recursion,
+\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993
+
+\bibitem{paulson-final}
+Paulson, L.~C.,
+\newblock A concrete final coalgebra theorem for {ZF} set theory,
+\newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994
+
+\bibitem{pelletier86}
+Pelletier, F.~J.,
+\newblock Seventy-five problems for testing automatic theorem provers,
+\newblock {\em J. Auto. Reas. {\bf 2}\/} (1986), 191--216,
+\newblock Errata, JAR 4 (1988), 235--236
+
+\bibitem{plaisted90}
+Plaisted, D.~A.,
+\newblock A sequent-style model elimination strategy and a positive refinement,
+\newblock {\em J. Auto. Reas. {\bf 6}}, 4 (1990), 389--402
+
+\bibitem{quaife92}
+Quaife, A.,
+\newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory,
+\newblock {\em J. Auto. Reas. {\bf 8}}, 1 (1992), 91--147
+
+\bibitem{sawamura92}
+Sawamura, H., Minami, T., Ohashi, K.,
+\newblock Proof methods based on sheet of thought in {EUODHILOS},
+\newblock Research Report IIAS-RR-92-6E, International Institute for Advanced
+  Study of Social Information Science, Fujitsu Laboratories, 1992
+
+\bibitem{suppes72}
+Suppes, P.,
+\newblock {\em Axiomatic Set Theory},
+\newblock Dover, 1972
+
+\bibitem{takeuti87}
+Takeuti, G.,
+\newblock {\em Proof Theory}, 2nd~ed.,
+\newblock North Holland, 1987
+
+\bibitem{thompson91}
+Thompson, S.,
+\newblock {\em Type Theory and Functional Programming},
+\newblock Addison-Wesley, 1991
+
+\bibitem{principia}
+Whitehead, A.~N., Russell, B.,
+\newblock {\em Principia Mathematica},
+\newblock Cambridge Univ. Press, 1962,
+\newblock Paperback edition to *56, abridged from the 2nd edition (1927)
+
+\bibitem{wos-bledsoe}
+Wos, L.,
+\newblock Automated reasoning and {Bledsoe's} dream for the field,
+\newblock In {\em Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
+  R.~S. Boyer, Ed. Kluwer Academic Publishers, 1991, pp.~297--342
+
+\end{thebibliography}