author  paulson 
Fri, 17 Jan 1997 12:49:31 +0100  
changeset 2516  4d68fbe6378b 
parent 2220  547d2b58307e 
child 2610  655dc064a28c 
permissions  rwrr 
104  1 
\begin{thebibliography}{10} 
2 

3 
\bibitem{abramsky90} 

293  4 
Abramsky, S., 
5 
\newblock The lazy lambda calculus, 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

6 
\newblock In {\em Research Topics in Functional Programming}, D.~A. Turner, Ed. 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

40 
\newblock In {\em Logical Frameworks}, G.~Huet G.~Plotkin, Eds. Cambridge Univ. 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

41 
Press, 1991, pp.~280306 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

42 

82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

43 
\bibitem{types94} 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

44 
Dybjer, P., Nordstr{\"om}, B., Smith, J., Eds., 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

45 
\newblock {\em Types for Proofs and Programs: International Workshop {TYPES 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

46 
'94}}, 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

47 
\newblock LNCS 996. Springer, published 1995 
293  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 

104  53 

1535  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 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

59 
\bibitem{gimenezcodifying} 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

60 
Gim{\'e}nez, E., 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

61 
\newblock Codifying guarded definitions with recursive schemes, 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

62 
\newblock In Dybjer et~al. \cite{types94}, pp.~3959 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

63 

82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

64 
\bibitem{guntertrees} 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

65 
Gunter, E.~L., 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

66 
\newblock A broader class of trees for recursive type definitions for {HOL}, 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

67 
\newblock In {\em Higher Order Logic Theorem Proving and Its Applications: HUG 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

68 
'93\/} (Published 1994), J.~Joyce C.~Seger, Eds., LNCS 780, Springer, 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

69 
pp.~141154 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

70 

104  71 
\bibitem{hennessy90} 
293  72 
Hennessy, M., 
104  73 
\newblock {\em The Semantics of Programming Languages: An Elementary 
293  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), 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

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

83 
\bibitem{melham89} 

293  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 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

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

89 
\bibitem{milnerind} 

90 
Milner, R., 

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

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

104  93 

94 
\bibitem{milner89} 

293  95 
Milner, R., 
96 
\newblock {\em Communication and Concurrency}, 

97 
\newblock PrenticeHall, 1989 

98 

1535  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 

293  104 
\bibitem{monahan84} 
105 
Monahan, B.~Q., 

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

107 
\newblock PhD thesis, University of Edinburgh, 1984 

104  108 

1535  109 
\bibitem{nipkowCR} 
110 
Nipkow, T., 

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

2136  112 
\newblock In {\em Automated Deduction  {CADE}13 International Conference\/} 
113 
(1996), M.~McRobbie J.~K. Slaney, Eds., LNAI 1104, Springer, pp.~733747 

1535  114 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

115 
\bibitem{pvslanguage} 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

116 
Owre, S., Shankar, N., Rushby, J.~M., 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

117 
\newblock {\em The {PVS} specification language}, 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

118 
\newblock Computer Science Laboratory, SRI International, Menlo Park, CA, Apr. 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

119 
1993, 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

120 
\newblock Beta release 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

121 

2220  122 
\bibitem{paulintlca} 
293  123 
PaulinMohring, C., 
124 
\newblock Inductive definitions in the system {Coq}: Rules and properties, 

2220  125 
\newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem 
126 
J.~Groote, Eds., LNCS 664, Springer, pp.~328345 

104  127 

2136  128 
\bibitem{paulsonmarkt} 
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 

293  135 
\bibitem{paulson87} 
136 
Paulson, L.~C., 

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

138 
\newblock Cambridge Univ. Press, 1987 

104  139 

293  140 
\bibitem{paulsonsetI} 
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), 353389 

104  144 

2136  145 
\bibitem{paulsonisabook} 
146 
Paulson, L.~C., 

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

148 
\newblock Springer, 1994, 

149 
\newblock LNCS 828 

150 

104  151 
\bibitem{paulsonsetII} 
293  152 
Paulson, L.~C., 
153 
\newblock Set theory for verification: {II}. {Induction} and recursion, 

1444  154 
\newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167215 
293  155 

1535  156 
\bibitem{paulsoncoind} 
157 
Paulson, L.~C., 

158 
\newblock Mechanizing coinduction and corecursion in higherorder logic, 

2136  159 
\newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), 
1535  160 
\newblock In press 
161 

293  162 
\bibitem{paulsonfinal} 
163 
Paulson, L.~C., 

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

165 
\newblock In Dybjer et~al. \cite{types94}, pp.~120139 
104  166 

1535  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.\/} (1996), 

171 
\newblock In press 

172 

104  173 
\bibitem{pitts94} 
293  174 
Pitts, A.~M., 
175 
\newblock A coinduction principle for recursively defined domains, 

606  176 
\newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195219 
293  177 

1535  178 
\bibitem{rasmussen95} 
179 
Rasmussen, O., 

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

181 
experiment, 

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

183 
1995 

184 

293  185 
\bibitem{saaltinkfme} 
186 
Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I., 

187 
\newblock An {EVES} data abstraction example, 

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

189 
J.~C.~P. Woodcock P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578596 
104  190 

1535  191 
\bibitem{slindtfl} 
192 
Slind, K., 

193 
\newblock Function definition in higherorder logic, 

1838  194 
\newblock In {\em Theorem Proving in Higher Order Logics\/} (1996), J.~von 
2136  195 
Wright, J.~Grundy, J.~Harrison, Eds., LNCS 1125 
1535  196 

104  197 
\bibitem{szasz93} 
293  198 
Szasz, N., 
104  199 
\newblock A machine checked proof that {Ackermann's} function is not primitive 
293  200 
recursive, 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1838
diff
changeset

201 
\newblock In {\em Logical Environments}, G.~Huet G.~Plotkin, Eds. Cambridge 
293  202 
Univ. Press, 1993, pp.~317338 
104  203 

1535  204 
\bibitem{voelker95} 
205 
V\"olker, N., 

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

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

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

209 
pp.~206218 

210 

211 
\bibitem{winskel93} 

212 
Winskel, G., 

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

214 
\newblock MIT Press, 1993 

215 

104  216 
\end{thebibliography} 