104

1 
\begin{thebibliography}{10}


2 


3 
\bibitem{abramsky90}

293

4 
Abramsky, S.,


5 
\newblock The lazy lambda calculus,


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


7 
Ed. AddisonWesley, 1977, pp.~65116

104

8 


9 
\bibitem{aczel77}

293

10 
Aczel, P.,


11 
\newblock An introduction to inductive definitions,


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


13 
NorthHolland, 1977, pp.~739782

104

14 


15 
\bibitem{aczel88}

293

16 
Aczel, P.,


17 
\newblock {\em NonWellFounded Sets},


18 
\newblock CSLI, 1988

104

19 


20 
\bibitem{bm79}

293

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


22 
\newblock {\em A Computational Logic},


23 
\newblock Academic Press, 1979

104

24 


25 
\bibitem{camilleri92}

293

26 
Camilleri, J., Melham, T.~F.,

104

27 
\newblock Reasoning with inductively defined relations in the {HOL} theorem

293

28 
prover,


29 
\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, August 1992

104

30 


31 
\bibitem{davey&priestley}

293

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


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


34 
\newblock Cambridge Univ. Press, 1990


35 


36 
\bibitem{dybjer91}


37 
Dybjer, P.,


38 
\newblock Inductive sets and families in {MartinL\"of's} type theory and their


39 
settheoretic semantics,


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


41 
Univ. Press, 1991, pp.~280306


42 


43 
\bibitem{IMPS}


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), 213248

104

47 


48 
\bibitem{hennessy90}

293

49 
Hennessy, M.,

104

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

293

51 
Introduction Using Structural Operational Semantics},


52 
\newblock Wiley, 1990


53 


54 
\bibitem{huet88}


55 
Huet, G.,


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


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


58 
Elsevier, pp.~205216

104

59 


60 
\bibitem{melham89}

293

61 
Melham, T.~F.,


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,


65 
pp.~341386


66 


67 
\bibitem{milnerind}


68 
Milner, R.,


69 
\newblock How to derive inductions in {LCF},


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

104

71 


72 
\bibitem{milner89}

293

73 
Milner, R.,


74 
\newblock {\em Communication and Concurrency},


75 
\newblock PrenticeHall, 1989


76 


77 
\bibitem{monahan84}


78 
Monahan, B.~Q.,


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


80 
\newblock PhD thesis, University of Edinburgh, 1984

104

81 


82 
\bibitem{paulin92}

293

83 
PaulinMohring, C.,


84 
\newblock Inductive definitions in the system {Coq}: Rules and properties,


85 
\newblock Research Report 9249, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.


86 
1992

104

87 

293

88 
\bibitem{paulson87}


89 
Paulson, L.~C.,


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


91 
\newblock Cambridge Univ. Press, 1987

104

92 


93 
\bibitem{paulson91}

293

94 
Paulson, L.~C.,


95 
\newblock {\em {ML} for the Working Programmer},


96 
\newblock Cambridge Univ. Press, 1991

104

97 


98 
\bibitem{paulsoncoind}

293

99 
Paulson, L.~C.,


100 
\newblock Coinduction and corecursion in higherorder logic,


101 
\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993

104

102 


103 
\bibitem{isabelleintro}

293

104 
Paulson, L.~C.,


105 
\newblock Introduction to {Isabelle},


106 
\newblock Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 1993


107 


108 
\bibitem{paulsonsetI}


109 
Paulson, L.~C.,


110 
\newblock Set theory for verification: {I}. {From} foundations to functions,


111 
\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353389

104

112 


113 
\bibitem{paulsonsetII}

293

114 
Paulson, L.~C.,


115 
\newblock Set theory for verification: {II}. {Induction} and recursion,


116 
\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993


117 


118 
\bibitem{paulsonfinal}


119 
Paulson, L.~C.,


120 
\newblock A concrete final coalgebra theorem for {ZF} set theory,


121 
\newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994

104

122 


123 
\bibitem{pitts94}

293

124 
Pitts, A.~M.,


125 
\newblock A coinduction principle for recursively defined domains,


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


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


128 


129 
\bibitem{saaltinkfme}


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


131 
\newblock An {EVES} data abstraction example,


132 
\newblock In {\em FME '93: IndustrialStrength Formal Methods\/} (1993),


133 
J.~C.~P. Woodcock, P.~G. Larsen, Eds., Springer, pp.~578596,


134 
\newblock LNCS 670

104

135 


136 
\bibitem{szasz93}

293

137 
Szasz, N.,

104

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

293

139 
recursive,


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


141 
Univ. Press, 1993, pp.~317338

104

142 


143 
\end{thebibliography}
