1 \begin{thebibliography}{10}
5 \newblock The lazy lambda calculus,
6 \newblock In {\em Research Topics in Functional Programming}, D.~A. Turner, Ed.
7 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, Aug. 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 Univ.
41 Press, 1991, pp.~280--306
44 Dybjer, P., Nordstr{\"om}, B., Smith, J., Eds.,
45 \newblock {\em Types for Proofs and Programs: International Workshop {TYPES
47 \newblock LNCS 996. Springer, published 1995
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), 213--248
56 \newblock A case study of co-induction in {Isabelle},
57 \newblock Tech. Rep. 359, Comp. Lab., Univ. Cambridge, Feb. 1995
59 \bibitem{gimenez-codifying}
61 \newblock Codifying guarded definitions with recursive schemes,
62 \newblock In Dybjer et~al. \cite{types94}, pp.~39--59
64 \bibitem{gunter-trees}
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,
73 \newblock {\em The Semantics of Programming Languages: An Elementary
74 Introduction Using Structural Operational Semantics},
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.~205--216
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.~341--386
91 \newblock How to derive inductions in {LCF},
92 \newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980
96 \newblock {\em Communication and Concurrency},
97 \newblock Prentice-Hall, 1989
99 \bibitem{milner-coind}
100 Milner, R., Tofte, M.,
101 \newblock Co-induction in relational semantics,
102 \newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
106 \newblock {\em Data Type Proofs using Edinburgh {LCF}},
107 \newblock PhD thesis, University of Edinburgh, 1984
111 \newblock More {Church-Rosser} 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.~733--747
115 \bibitem{pvs-language}
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.
120 \newblock Beta release
122 \bibitem{paulin-tlca}
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.~328--345
128 \bibitem{paulson-markt}
130 \newblock Tool support for logics of programs,
131 \newblock In {\em Mathematical Methods in Program Development: Summer School
132 Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer,
137 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
138 \newblock Cambridge Univ. Press, 1987
140 \bibitem{paulson-set-I}
142 \newblock Set theory for verification: {I}. {From} foundations to functions,
143 \newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
145 \bibitem{paulson-isa-book}
147 \newblock {\em Isabelle: A Generic Theorem Prover},
148 \newblock Springer, 1994,
151 \bibitem{paulson-set-II}
153 \newblock Set theory for verification: {II}. {Induction} and recursion,
154 \newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215
156 \bibitem{paulson-coind}
158 \newblock Mechanizing coinduction and corecursion in higher-order logic,
159 \newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), 175--204
161 \bibitem{paulson-final}
163 \newblock A concrete final coalgebra theorem for {ZF} set theory,
164 \newblock In Dybjer et~al. \cite{types94}, pp.~120--139
167 Paulson, L.~C., Gr\c{a}bczewski, K.,
168 \newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice,
169 \newblock {\em J. Auto. Reas. {\bf 17}}, 3 (Dec. 1996), 291--323
173 \newblock A co-induction principle for recursively defined domains,
174 \newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219
176 \bibitem{rasmussen95}
178 \newblock The {Church-Rosser} theorem in {Isabelle}: A proof porting
180 \newblock Tech. Rep. 364, Computer Laboratory, University of Cambridge, May
183 \bibitem{saaltink-fme}
184 Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
185 \newblock An {EVES} data abstraction example,
186 \newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
187 J.~C.~P. Woodcock P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596
191 \newblock Function definition in higher-order logic,
192 \newblock In {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96\/}
193 (1996), J.~von Wright, J.~Grundy, J.~Harrison, Eds., LNCS 1125
197 \newblock A machine checked proof that {Ackermann's} function is not primitive
199 \newblock In {\em Logical Environments}, G.~Huet G.~Plotkin, Eds. Cambridge
200 Univ. Press, 1993, pp.~317--338
204 \newblock On the representation of datatypes in {Isabelle/HOL},
205 \newblock In {\em Proceedings of the First Isabelle Users Workshop\/} (Sept.
206 1995), L.~C. Paulson, Ed., Technical Report 379, Comp. Lab., Univ. Cambridge,
211 \newblock {\em The Formal Semantics of Programming Languages},
212 \newblock MIT Press, 1993
214 \end{thebibliography}