\begin{thebibliography}{10}

\bibitem{abramsky90}

Abramsky, S.,

\newblock The lazy lambda calculus,

\newblock In {\em Resesarch Topics in Functional Programming}, D.~A. Turner,

  Ed. Addison-Wesley, 1977, pp.~65--116

\bibitem{aczel77}

Aczel, P.,

\newblock An introduction to inductive definitions,

\newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed.

  North-Holland, 1977, pp.~739--782

\bibitem{aczel88}

Aczel, P.,

\newblock {\em Non-Well-Founded Sets},

\newblock CSLI, 1988

\bibitem{bm79}

Boyer, R.~S., Moore, J.~S.,

\newblock {\em A Computational Logic},

\newblock Academic Press, 1979

\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, August 1992

\bibitem{davey&priestley}

Davey, B.~A., Priestley, H.~A.,

\newblock {\em Introduction to Lattices and Order},

\newblock Cambridge Univ. Press, 1990

\bibitem{dybjer91}

Dybjer, P.,

\newblock Inductive sets and families in {Martin-L\"of's} type theory and their

  set-theoretic semantics,

\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge

  Univ. Press, 1991, pp.~280--306

\bibitem{IMPS}

Farmer, W.~M., Guttman, J.~D., Thayer, F.~J.,

\newblock {IMPS}: An interactive mathematical proof system,

\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248

\bibitem{hennessy90}

Hennessy, M.,

\newblock {\em The Semantics of Programming Languages: An Elementary

  Introduction Using Structural Operational Semantics},

\newblock Wiley, 1990

\bibitem{huet88}

Huet, G.,

\newblock Induction principles formalized in the {Calculus of Constructions},

\newblock In {\em Programming of Future Generation Computers\/} (1988),

  Elsevier, pp.~205--216

\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{milner-ind}

Milner, R.,

\newblock How to derive inductions in {LCF},

\newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980

\bibitem{milner89}

Milner, R.,

\newblock {\em Communication and Concurrency},

\newblock Prentice-Hall, 1989

\bibitem{monahan84}

Monahan, B.~Q.,

\newblock {\em Data Type Proofs using Edinburgh {LCF}},

\newblock PhD thesis, University of Edinburgh, 1984

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

Paulson, L.~C.,

\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},

\newblock Cambridge Univ. Press, 1987

\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{isabelle-intro}

Paulson, L.~C.,

\newblock Introduction to {Isabelle},

\newblock Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 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{pitts94}

Pitts, A.~M.,

\newblock A co-induction principle for recursively defined domains,

\newblock {\em Theoretical Comput. Sci.\/} (1994),

\newblock In press; available as Report 252, Comp. Lab., Univ. Cambridge

\bibitem{saaltink-fme}

Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,

\newblock An {EVES} data abstraction example,

\newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),

  J.~C.~P. Woodcock, P.~G. Larsen, Eds., Springer, pp.~578--596,

\newblock LNCS 670

\bibitem{szasz93}

Szasz, N.,

\newblock A machine checked proof that {Ackermann's} function is not primitive

  recursive,

\newblock In {\em Logical Environments}, G.~Huet, G.~Plotkin, Eds. Cambridge

  Univ. Press, 1993, pp.~317--338

\end{thebibliography}