|
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 Addison-Wesley, 1977, pp.~65--116 |
|
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 North-Holland, 1977, pp.~739--782 |
|
14 |
|
15 \bibitem{aczel88} |
|
16 Aczel, P., |
|
17 \newblock {\em Non-Well-Founded 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 {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 |
|
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), 213--248 |
|
53 |
|
54 \bibitem{frost95} |
|
55 Frost, J., |
|
56 \newblock A case study of co-induction in {Isabelle}, |
|
57 \newblock Tech. Rep. 359, Comp. Lab., Univ. Cambridge, Feb. 1995 |
|
58 |
|
59 \bibitem{gimenez-codifying} |
|
60 Gim{\'e}nez, E., |
|
61 \newblock Codifying guarded definitions with recursive schemes, |
|
62 \newblock In Dybjer et~al. \cite{types94}, pp.~39--59 |
|
63 |
|
64 \bibitem{gunter-trees} |
|
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.~141--154 |
|
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.~205--216 |
|
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.~341--386 |
|
88 |
|
89 \bibitem{milner-ind} |
|
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 Prentice-Hall, 1989 |
|
98 |
|
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 |
|
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{nipkow-CR} |
|
110 Nipkow, T., |
|
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 |
|
114 |
|
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. |
|
119 1993, |
|
120 \newblock Beta release |
|
121 |
|
122 \bibitem{paulin-tlca} |
|
123 Paulin-Mohring, 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.~328--345 |
|
127 |
|
128 \bibitem{paulson-markt} |
|
129 Paulson, L.~C., |
|
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, |
|
133 \newblock In press |
|
134 |
|
135 \bibitem{paulson87} |
|
136 Paulson, L.~C., |
|
137 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}, |
|
138 \newblock Cambridge Univ. Press, 1987 |
|
139 |
|
140 \bibitem{paulson-set-I} |
|
141 Paulson, L.~C., |
|
142 \newblock Set theory for verification: {I}. {From} foundations to functions, |
|
143 \newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389 |
|
144 |
|
145 \bibitem{paulson-isa-book} |
|
146 Paulson, L.~C., |
|
147 \newblock {\em Isabelle: A Generic Theorem Prover}, |
|
148 \newblock Springer, 1994, |
|
149 \newblock LNCS 828 |
|
150 |
|
151 \bibitem{paulson-set-II} |
|
152 Paulson, L.~C., |
|
153 \newblock Set theory for verification: {II}. {Induction} and recursion, |
|
154 \newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215 |
|
155 |
|
156 \bibitem{paulson-coind} |
|
157 Paulson, L.~C., |
|
158 \newblock Mechanizing coinduction and corecursion in higher-order logic, |
|
159 \newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), 175--204 |
|
160 |
|
161 \bibitem{paulson-final} |
|
162 Paulson, L.~C., |
|
163 \newblock A concrete final coalgebra theorem for {ZF} set theory, |
|
164 \newblock In Dybjer et~al. \cite{types94}, pp.~120--139 |
|
165 |
|
166 \bibitem{paulson-gr} |
|
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 |
|
170 |
|
171 \bibitem{pitts94} |
|
172 Pitts, A.~M., |
|
173 \newblock A co-induction principle for recursively defined domains, |
|
174 \newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219 |
|
175 |
|
176 \bibitem{rasmussen95} |
|
177 Rasmussen, O., |
|
178 \newblock The {Church-Rosser} theorem in {Isabelle}: A proof porting |
|
179 experiment, |
|
180 \newblock Tech. Rep. 364, Computer Laboratory, University of Cambridge, May |
|
181 1995 |
|
182 |
|
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 |
|
188 |
|
189 \bibitem{slind-tfl} |
|
190 Slind, K., |
|
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 |
|
194 |
|
195 \bibitem{szasz93} |
|
196 Szasz, N., |
|
197 \newblock A machine checked proof that {Ackermann's} function is not primitive |
|
198 recursive, |
|
199 \newblock In {\em Logical Environments}, G.~Huet G.~Plotkin, Eds. Cambridge |
|
200 Univ. Press, 1993, pp.~317--338 |
|
201 |
|
202 \bibitem{voelker95} |
|
203 V\"olker, N., |
|
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, |
|
207 pp.~206--218 |
|
208 |
|
209 \bibitem{winskel93} |
|
210 Winskel, G., |
|
211 \newblock {\em The Formal Semantics of Programming Languages}, |
|
212 \newblock MIT Press, 1993 |
|
213 |
|
214 \end{thebibliography} |