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