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,

606

29 
\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 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 

1535

48 
\bibitem{frost95}


49 
Frost, J.,


50 
\newblock A case study of coinduction in {Isabelle},


51 
\newblock Tech. Rep. 359, Comp. Lab., Univ. Cambridge, Feb. 1995


52 

104

53 
\bibitem{hennessy90}

293

54 
Hennessy, M.,

104

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

293

56 
Introduction Using Structural Operational Semantics},


57 
\newblock Wiley, 1990


58 


59 
\bibitem{huet88}


60 
Huet, G.,


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


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

1444

63 
K.~Fuchi, M.~Nivat, Eds., Elsevier, pp.~205216

104

64 


65 
\bibitem{melham89}

293

66 
Melham, T.~F.,


67 
\newblock Automating recursive type definitions in higher order logic,


68 
\newblock In {\em Current Trends in Hardware Verification and Automated Theorem


69 
Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,


70 
pp.~341386


71 


72 
\bibitem{milnerind}


73 
Milner, R.,


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


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

104

76 


77 
\bibitem{milner89}

293

78 
Milner, R.,


79 
\newblock {\em Communication and Concurrency},


80 
\newblock PrenticeHall, 1989


81 

1535

82 
\bibitem{milnercoind}


83 
Milner, R., Tofte, M.,


84 
\newblock Coinduction in relational semantics,


85 
\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209220


86 

293

87 
\bibitem{monahan84}


88 
Monahan, B.~Q.,


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


90 
\newblock PhD thesis, University of Edinburgh, 1984

104

91 

1535

92 
\bibitem{nipkowCR}


93 
Nipkow, T.,


94 
\newblock More {ChurchRosser} proofs (in {Isabelle/HOL}),


95 
\newblock Tech. rep., T. U. Munich, 1996


96 

104

97 
\bibitem{paulin92}

293

98 
PaulinMohring, C.,


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


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


101 
1992

104

102 

293

103 
\bibitem{paulson87}


104 
Paulson, L.~C.,


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


106 
\newblock Cambridge Univ. Press, 1987

104

107 


108 
\bibitem{isabelleintro}

293

109 
Paulson, L.~C.,


110 
\newblock Introduction to {Isabelle},


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


112 


113 
\bibitem{paulsonsetI}


114 
Paulson, L.~C.,


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


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

104

117 


118 
\bibitem{paulsonsetII}

293

119 
Paulson, L.~C.,


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

1444

121 
\newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167215

293

122 

1535

123 
\bibitem{paulsoncoind}


124 
Paulson, L.~C.,


125 
\newblock Mechanizing coinduction and corecursion in higherorder logic,


126 
\newblock {\em J. Logic and Comput.\/} (1996),


127 
\newblock In press


128 

293

129 
\bibitem{paulsonfinal}


130 
Paulson, L.~C.,


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

1444

132 
\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES


133 
'94}\/} (published 1995), P.~Dybjer, B.~Nordstr{\"om},, J.~Smith, Eds., LNCS


134 
996, Springer, pp.~120139

104

135 

1535

136 
\bibitem{paulsongr}


137 
Paulson, L.~C., Gr\c{a}bczewski, K.,


138 
\newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice,


139 
\newblock {\em J. Auto. Reas.\/} (1996),


140 
\newblock In press


141 

104

142 
\bibitem{pitts94}

293

143 
Pitts, A.~M.,


144 
\newblock A coinduction principle for recursively defined domains,

606

145 
\newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195219

293

146 

1535

147 
\bibitem{rasmussen95}


148 
Rasmussen, O.,


149 
\newblock The {ChurchRosser} theorem in {Isabelle}: A proof porting


150 
experiment,


151 
\newblock Tech. Rep. 364, Computer Laboratory, University of Cambridge, May


152 
1995


153 

293

154 
\bibitem{saaltinkfme}


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


156 
\newblock An {EVES} data abstraction example,


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

1444

158 
J.~C.~P. Woodcock, P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578596

104

159 

1535

160 
\bibitem{slindtfl}


161 
Slind, K.,


162 
\newblock Function definition in higherorder logic,


163 
\newblock Tech. rep., T. U. Munich, 1996


164 

104

165 
\bibitem{szasz93}

293

166 
Szasz, N.,

104

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

293

168 
recursive,


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


170 
Univ. Press, 1993, pp.~317338

104

171 

1535

172 
\bibitem{voelker95}


173 
V\"olker, N.,


174 
\newblock On the representation of datatypes in {Isabelle/HOL},


175 
\newblock In {\em Proceedings of the First Isabelle Users Workshop\/} (Sept.


176 
1995), L.~C. Paulson, Ed., Technical Report 379, Comp. Lab., Univ. Cambridge,


177 
pp.~206218


178 


179 
\bibitem{winskel93}


180 
Winskel, G.,


181 
\newblock {\em The Formal Semantics of Programming Languages},


182 
\newblock MIT Press, 1993


183 

104

184 
\end{thebibliography}
