1 \begin{thebibliography}{10}
5 \newblock The lazy lambda calculus,
6 \newblock In {\em Resesarch Topics in Functional Programming}, D.~A. Turner,
7 Ed. Addison-Wesley, 1977, pp.~65--116
11 \newblock An introduction to inductive definitions,
12 \newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed.
13 North-Holland, 1977, pp.~739--782
17 \newblock {\em Non-Well-Founded Sets},
21 Boyer, R.~S., Moore, J.~S.,
22 \newblock {\em A Computational Logic},
23 \newblock Academic Press, 1979
26 Camilleri, J., Melham, T.~F.,
27 \newblock Reasoning with inductively defined relations in the {HOL} theorem
29 \newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, August 1992
31 \bibitem{davey&priestley}
32 Davey, B.~A., Priestley, H.~A.,
33 \newblock {\em Introduction to Lattices and Order},
34 \newblock Cambridge Univ. Press, 1990
38 \newblock Inductive sets and families in {Martin-L\"of's} type theory and their
39 set-theoretic semantics,
40 \newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge
41 Univ. Press, 1991, pp.~280--306
44 Farmer, W.~M., Guttman, J.~D., Thayer, F.~J.,
45 \newblock {IMPS}: An interactive mathematical proof system,
46 \newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248
50 \newblock {\em The Semantics of Programming Languages: An Elementary
51 Introduction Using Structural Operational Semantics},
56 \newblock Induction principles formalized in the {Calculus of Constructions},
57 \newblock In {\em Programming of Future Generation Computers\/} (1988),
58 Elsevier, pp.~205--216
62 \newblock Automating recursive type definitions in higher order logic,
63 \newblock In {\em Current Trends in Hardware Verification and Automated Theorem
64 Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,
69 \newblock How to derive inductions in {LCF},
70 \newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980
74 \newblock {\em Communication and Concurrency},
75 \newblock Prentice-Hall, 1989
79 \newblock {\em Data Type Proofs using Edinburgh {LCF}},
80 \newblock PhD thesis, University of Edinburgh, 1984
84 \newblock Inductive definitions in the system {Coq}: Rules and properties,
85 \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.
90 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
91 \newblock Cambridge Univ. Press, 1987
95 \newblock {\em {ML} for the Working Programmer},
96 \newblock Cambridge Univ. Press, 1991
98 \bibitem{paulson-coind}
100 \newblock Co-induction and co-recursion in higher-order logic,
101 \newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
103 \bibitem{isabelle-intro}
105 \newblock Introduction to {Isabelle},
106 \newblock Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 1993
108 \bibitem{paulson-set-I}
110 \newblock Set theory for verification: {I}. {From} foundations to functions,
111 \newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
113 \bibitem{paulson-set-II}
115 \newblock Set theory for verification: {II}. {Induction} and recursion,
116 \newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993
118 \bibitem{paulson-final}
120 \newblock A concrete final coalgebra theorem for {ZF} set theory,
121 \newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994
125 \newblock A co-induction principle for recursively defined domains,
126 \newblock {\em Theoretical Comput. Sci.\/} (1994),
127 \newblock In press; available as Report 252, Comp. Lab., Univ. Cambridge
129 \bibitem{saaltink-fme}
130 Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
131 \newblock An {EVES} data abstraction example,
132 \newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
133 J.~C.~P. Woodcock, P.~G. Larsen, Eds., Springer, pp.~578--596,
138 \newblock A machine checked proof that {Ackermann's} function is not primitive
140 \newblock In {\em Logical Environments}, G.~Huet, G.~Plotkin, Eds. Cambridge
141 Univ. Press, 1993, pp.~317--338
143 \end{thebibliography}