3162

1 
\begin{thebibliography}{10}


2 


3 
\bibitem{abramsky90}


4 
Abramsky, S.,


5 
\newblock The lazy lambda calculus,


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


7 
AddisonWesley, 1977, pp.~65116


8 


9 
\bibitem{aczel77}


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


14 


15 
\bibitem{aczel88}


16 
Aczel, P.,


17 
\newblock {\em NonWellFounded Sets},


18 
\newblock CSLI, 1988


19 


20 
\bibitem{bm79}


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


22 
\newblock {\em A Computational Logic},


23 
\newblock Academic Press, 1979


24 


25 
\bibitem{camilleri92}


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


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


28 
prover,


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


30 


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


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 Univ.


41 
Press, 1991, pp.~280306


42 


43 
\bibitem{types94}


44 
Dybjer, P., Nordstr{\"om}, B., Smith, J., Eds.,


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


46 
'94}},


47 
\newblock LNCS 996. Springer, published 1995


48 


49 
\bibitem{IMPS}


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


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


52 
\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213248


53 


54 
\bibitem{frost95}


55 
Frost, J.,


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


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


58 


59 
\bibitem{gimenezcodifying}


60 
Gim{\'e}nez, E.,


61 
\newblock Codifying guarded definitions with recursive schemes,


62 
\newblock In Dybjer et~al. \cite{types94}, pp.~3959


63 


64 
\bibitem{guntertrees}


65 
Gunter, E.~L.,


66 
\newblock A broader class of trees for recursive type definitions for {HOL},


67 
\newblock In {\em Higher Order Logic Theorem Proving and Its Applications: HUG


68 
'93\/} (Published 1994), J.~Joyce C.~Seger, Eds., LNCS 780, Springer,


69 
pp.~141154


70 


71 
\bibitem{hennessy90}


72 
Hennessy, M.,


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


74 
Introduction Using Structural Operational Semantics},


75 
\newblock Wiley, 1990


76 


77 
\bibitem{huet88}


78 
Huet, G.,


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


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


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


82 


83 
\bibitem{melham89}


84 
Melham, T.~F.,


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


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


87 
Proving}, G.~Birtwistle P.~A. Subrahmanyam, Eds. Springer, 1989, pp.~341386


88 


89 
\bibitem{milnerind}


90 
Milner, R.,


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


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


93 


94 
\bibitem{milner89}


95 
Milner, R.,


96 
\newblock {\em Communication and Concurrency},


97 
\newblock PrenticeHall, 1989


98 


99 
\bibitem{milnercoind}


100 
Milner, R., Tofte, M.,


101 
\newblock Coinduction in relational semantics,


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


103 


104 
\bibitem{monahan84}


105 
Monahan, B.~Q.,


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


107 
\newblock PhD thesis, University of Edinburgh, 1984


108 


109 
\bibitem{nipkowCR}


110 
Nipkow, T.,


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


112 
\newblock In {\em Automated Deduction  {CADE}13 International Conference\/}


113 
(1996), M.~McRobbie J.~K. Slaney, Eds., LNAI 1104, Springer, pp.~733747


114 


115 
\bibitem{pvslanguage}


116 
Owre, S., Shankar, N., Rushby, J.~M.,


117 
\newblock {\em The {PVS} specification language},


118 
\newblock Computer Science Laboratory, SRI International, Menlo Park, CA, Apr.


119 
1993,


120 
\newblock Beta release


121 


122 
\bibitem{paulintlca}


123 
PaulinMohring, C.,


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


125 
\newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem


126 
J.~Groote, Eds., LNCS 664, Springer, pp.~328345


127 


128 
\bibitem{paulson87}


129 
Paulson, L.~C.,


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


131 
\newblock Cambridge Univ. Press, 1987


132 


133 
\bibitem{paulsonsetI}


134 
Paulson, L.~C.,


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


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


137 


138 
\bibitem{paulsonisabook}


139 
Paulson, L.~C.,


140 
\newblock {\em Isabelle: A Generic Theorem Prover},


141 
\newblock Springer, 1994,


142 
\newblock LNCS 828


143 


144 
\bibitem{paulsonsetII}


145 
Paulson, L.~C.,


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


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


148 


149 
\bibitem{paulsoncoind}


150 
Paulson, L.~C.,


151 
\newblock Mechanizing coinduction and corecursion in higherorder logic,


152 
\newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), 175204


153 


154 
\bibitem{paulsonfinal}


155 
Paulson, L.~C.,


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


157 
\newblock In Dybjer et~al. \cite{types94}, pp.~120139


158 

4058

159 
\bibitem{paulsonmarkt}


160 
Paulson, L.~C.,


161 
\newblock Tool support for logics of programs,


162 
\newblock In {\em Mathematical Methods in Program Development: Summer School


163 
Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer, Published


164 
1997,


165 
\newblock In press


166 

3162

167 
\bibitem{paulsongr}


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


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


170 
\newblock {\em J. Auto. Reas. {\bf 17}}, 3 (Dec. 1996), 291323


171 


172 
\bibitem{pitts94}


173 
Pitts, A.~M.,


174 
\newblock A coinduction principle for recursively defined domains,


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


176 


177 
\bibitem{rasmussen95}


178 
Rasmussen, O.,


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


180 
experiment,


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


182 
1995


183 


184 
\bibitem{saaltinkfme}


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


186 
\newblock An {EVES} data abstraction example,


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


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


189 


190 
\bibitem{slindtfl}


191 
Slind, K.,


192 
\newblock Function definition in higherorder logic,


193 
\newblock In {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96\/}


194 
(1996), J.~von Wright, J.~Grundy, J.~Harrison, Eds., LNCS 1125


195 


196 
\bibitem{szasz93}


197 
Szasz, N.,


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


199 
recursive,


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


201 
Univ. Press, 1993, pp.~317338


202 


203 
\bibitem{voelker95}


204 
V\"olker, N.,


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


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


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


208 
pp.~206218


209 


210 
\bibitem{winskel93}


211 
Winskel, G.,


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


213 
\newblock MIT Press, 1993


214 


215 
\end{thebibliography}
