\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}