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

1682

95 
\newblock In {\em Automated Deduction  {CADE}13\/} (1996), M.~McRobbie,


96 
J.~Slaney, Eds., LNAI, Springer, p.~?,


97 
\newblock in press

1535

98 

104

99 
\bibitem{paulin92}

293

100 
PaulinMohring, C.,


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


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


103 
1992

104

104 

293

105 
\bibitem{paulson87}


106 
Paulson, L.~C.,


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


108 
\newblock Cambridge Univ. Press, 1987

104

109 


110 
\bibitem{isabelleintro}

293

111 
Paulson, L.~C.,


112 
\newblock Introduction to {Isabelle},


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


114 


115 
\bibitem{paulsonsetI}


116 
Paulson, L.~C.,


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


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

104

119 


120 
\bibitem{paulsonsetII}

293

121 
Paulson, L.~C.,


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

1444

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

293

124 

1535

125 
\bibitem{paulsoncoind}


126 
Paulson, L.~C.,


127 
\newblock Mechanizing coinduction and corecursion in higherorder logic,


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


129 
\newblock In press


130 

293

131 
\bibitem{paulsonfinal}


132 
Paulson, L.~C.,


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

1444

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


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


136 
996, Springer, pp.~120139

104

137 

1535

138 
\bibitem{paulsongr}


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


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


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


142 
\newblock In press


143 

104

144 
\bibitem{pitts94}

293

145 
Pitts, A.~M.,


146 
\newblock A coinduction principle for recursively defined domains,

606

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

293

148 

1535

149 
\bibitem{rasmussen95}


150 
Rasmussen, O.,


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


152 
experiment,


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


154 
1995


155 

293

156 
\bibitem{saaltinkfme}


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


158 
\newblock An {EVES} data abstraction example,


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

1444

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

104

161 

1535

162 
\bibitem{slindtfl}


163 
Slind, K.,


164 
\newblock Function definition in higherorder logic,

1838

165 
\newblock In {\em Theorem Proving in Higher Order Logics\/} (1996), J.~von


166 
Wright, Ed.,


167 
\newblock In press

1535

168 

104

169 
\bibitem{szasz93}

293

170 
Szasz, N.,

104

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

293

172 
recursive,


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


174 
Univ. Press, 1993, pp.~317338

104

175 

1535

176 
\bibitem{voelker95}


177 
V\"olker, N.,


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


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


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


181 
pp.~206218


182 


183 
\bibitem{winskel93}


184 
Winskel, G.,


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


186 
\newblock MIT Press, 1993


187 

104

188 
\end{thebibliography}
