104

1 
\begin{thebibliography}{10}


2 

598

3 
\bibitem{abrial93}


4 
J.~R. Abrial and G.~Laffitte.


5 
\newblock Towards the mechanization of the proofs of some classical theorems of


6 
set theory.


7 
\newblock preprint, February 1993.


8 

104

9 
\bibitem{andrews86}


10 
Peter~B. Andrews.


11 
\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth


12 
Through Proof}.


13 
\newblock Academic Press, 1986.


14 

114

15 
\bibitem{basin91}


16 
David Basin and Matt Kaufmann.


17 
\newblock The {BoyerMoore} prover and {Nuprl}: An experimental comparison.


18 
\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical

598

19 
Frameworks}, pages 89119. Cambridge University Press, 1991.

114

20 

104

21 
\bibitem{boyer86}


22 
Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and


23 
Lawrence Wos.


24 
\newblock Set theory in firstorder logic: Clauses for {G\"odel's} axioms.

598

25 
\newblock {\em Journal of Automated Reasoning}, 2(3):287327, 1986.

114

26 


27 
\bibitem{camilleri92}


28 
J.~Camilleri and T.~F. Melham.


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


30 
prover.

598

31 
\newblock Technical Report 265, Computer Laboratory, University of Cambridge,


32 
August 1992.

104

33 


34 
\bibitem{church40}


35 
Alonzo Church.


36 
\newblock A formulation of the simple theory of types.

598

37 
\newblock {\em Journal of Symbolic Logic}, 5:5668, 1940.

359

38 


39 
\bibitem{coen92}


40 
Martin~D. Coen.


41 
\newblock {\em Interactive Program Derivation}.


42 
\newblock PhD thesis, University of Cambridge, 1992.


43 
\newblock Computer Laboratory Technical Report 272.


44 


45 
\bibitem{constable86}


46 
R.~L. {Constable et al.}


47 
\newblock {\em Implementing Mathematics with the Nuprl Proof Development


48 
System}.

598

49 
\newblock PrenticeHall, 1986.

359

50 


51 
\bibitem{davey&priestley}


52 
B.~A. Davey and H.~A. Priestley.


53 
\newblock {\em Introduction to Lattices and Order}.

598

54 
\newblock Cambridge University Press, 1990.

359

55 


56 
\bibitem{devlin79}


57 
Keith~J. Devlin.


58 
\newblock {\em Fundamentals of Contemporary Set Theory}.


59 
\newblock Springer, 1979.

104

60 


61 
\bibitem{dummett}


62 
Michael Dummett.


63 
\newblock {\em Elements of Intuitionism}.

114

64 
\newblock Oxford University Press, 1977.

104

65 


66 
\bibitem{dyckhoff}


67 
Roy Dyckhoff.


68 
\newblock Contractionfree sequent calculi for intuitionistic logic.

598

69 
\newblock {\em Journal of Symbolic Logic}, 57(3):795807, 1992.

104

70 


71 
\bibitem{felty91a}


72 
Amy Felty.


73 
\newblock A logic program for transforming sequent proofs to natural deduction


74 
proofs.


75 
\newblock In Peter SchroederHeister, editor, {\em Extensions of Logic


76 
Programming}, pages 157178. Springer, 1991.


77 
\newblock LNAI 475.


78 

114

79 
\bibitem{frost93}


80 
Jacob Frost.


81 
\newblock A case study of coinduction in {Isabelle HOL}.

598

82 
\newblock Technical Report 308, Computer Laboratory, University of Cambridge,


83 
August 1993.

104

84 


85 
\bibitem{gallier86}


86 
J.~H. Gallier.


87 
\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem


88 
Proving}.


89 
\newblock Harper \& Row, 1986.


90 

359

91 
\bibitem{mgordonhol}


92 
M.~J.~C. Gordon and T.~F. Melham.


93 
\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher


94 
Order Logic}.

598

95 
\newblock Cambridge University Press, 1993.

104

96 


97 
\bibitem{halmos60}


98 
Paul~R. Halmos.


99 
\newblock {\em Naive Set Theory}.


100 
\newblock Van Nostrand, 1960.


101 


102 
\bibitem{huet78}


103 
G.~P. Huet and B.~Lang.


104 
\newblock Proving and applying program transformations expressed with


105 
secondorder patterns.


106 
\newblock {\em Acta Informatica}, 11:3155, 1978.


107 

598

108 
\bibitem{kunen80}


109 
Kenneth Kunen.


110 
\newblock {\em Set Theory: An Introduction to Independence Proofs}.


111 
\newblock NorthHolland, 1980.


112 

359

113 
\bibitem{alf}


114 
Lena Magnusson and Bengt {Nordstr\"om}.


115 
\newblock The {ALF} proof editor and its proof engine.

598

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


117 
'93}}, pages 213237. Springer, published 1994.

359

118 
\newblock LNCS 806.


119 

114

120 
\bibitem{mw81}


121 
Zohar Manna and Richard Waldinger.


122 
\newblock Deductive synthesis of the unification algorithm.


123 
\newblock {\em Science of Computer Programming}, 1(1):548, 1981.


124 

104

125 
\bibitem{martinlof84}


126 
Per MartinL\"of.


127 
\newblock {\em Intuitionistic type theory}.


128 
\newblock Bibliopolis, 1984.


129 

359

130 
\bibitem{melham89}


131 
Thomas~F. Melham.


132 
\newblock Automating recursive type definitions in higher order logic.


133 
\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em Current


134 
Trends in Hardware Verification and Automated Theorem Proving}, pages


135 
341386. Springer, 1989.


136 

114

137 
\bibitem{milnercoind}


138 
Robin Milner and Mads Tofte.


139 
\newblock Coinduction in relational semantics.


140 
\newblock {\em Theoretical Computer Science}, 87:209220, 1991.

104

141 


142 
\bibitem{noel}


143 
Philippe {No\"el}.


144 
\newblock Experimenting with {Isabelle} in {ZF} set theory.

598

145 
\newblock {\em Journal of Automated Reasoning}, 10(1):1558, 1993.

104

146 


147 
\bibitem{nordstrom90}


148 
Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.


149 
\newblock {\em Programming in {MartinL\"of}'s Type Theory. An Introduction}.

114

150 
\newblock Oxford University Press, 1990.


151 


152 
\bibitem{paulin92}


153 
Christine PaulinMohring.


154 
\newblock Inductive definitions in the system {Coq}: Rules and properties.


155 
\newblock Research Report 9249, LIP, Ecole Normale Sup\'erieure de Lyon,


156 
December 1992.


157 


158 
\bibitem{paulson85}


159 
Lawrence~C. Paulson.


160 
\newblock Verifying the unification algorithm in {LCF}.


161 
\newblock {\em Science of Computer Programming}, 5:143170, 1985.

104

162 


163 
\bibitem{paulson87}


164 
Lawrence~C. Paulson.


165 
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.

598

166 
\newblock Cambridge University Press, 1987.

104

167 


168 
\bibitem{paulsonCOLOG}


169 
Lawrence~C. Paulson.


170 
\newblock A formulation of the simple theory of types (for {Isabelle}).


171 
\newblock In P.~MartinL\"of and G.~Mints, editors, {\em COLOG88:


172 
International Conference on Computer Logic}, Tallinn, 1990. Estonian Academy


173 
of Sciences, Springer.


174 
\newblock LNCS 417.


175 

114

176 
\bibitem{paulsoncoind}


177 
Lawrence~C. Paulson.


178 
\newblock Coinduction and corecursion in higherorder logic.

598

179 
\newblock Technical Report 304, Computer Laboratory, University of Cambridge,


180 
July 1993.

359

181 


182 
\bibitem{paulsonsetI}


183 
Lawrence~C. Paulson.


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

598

185 
\newblock {\em Journal of Automated Reasoning}, 11(3):353389, 1993.

114

186 


187 
\bibitem{paulsonsetII}


188 
Lawrence~C. Paulson.


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

598

190 
\newblock Technical Report 312, Computer Laboratory, University of Cambridge,


191 
1993.

359

192 


193 
\bibitem{paulsonfinal}


194 
Lawrence~C. Paulson.


195 
\newblock A concrete final coalgebra theorem for {ZF} set theory.

598

196 
\newblock Technical Report 334, Computer Laboratory, University of Cambridge,


197 
1994.


198 


199 
\bibitem{paulsonCADE}


200 
Lawrence~C. Paulson.


201 
\newblock A fixedpoint approach to implementing (co)inductive definitions.


202 
\newblock In Alan Bundy, editor, {\em 12th International Conference on


203 
Automated Deduction}, pages 148161. Springer, 1994.


204 
\newblock LNAI 814.

114

205 

104

206 
\bibitem{pelletier86}


207 
F.~J. Pelletier.


208 
\newblock Seventyfive problems for testing automatic theorem provers.

598

209 
\newblock {\em Journal of Automated Reasoning}, 2:191216, 1986.

104

210 
\newblock Errata, JAR 4 (1988), 235236.


211 


212 
\bibitem{plaisted90}


213 
David~A. Plaisted.


214 
\newblock A sequentstyle model elimination strategy and a positive refinement.

598

215 
\newblock {\em Journal of Automated Reasoning}, 6(4):389402, 1990.

104

216 


217 
\bibitem{quaife92}


218 
Art Quaife.


219 
\newblock Automated deduction in {von NeumannBernaysG\"odel} set theory.

598

220 
\newblock {\em Journal of Automated Reasoning}, 8(1):91147, 1992.

104

221 


222 
\bibitem{suppes72}


223 
Patrick Suppes.


224 
\newblock {\em Axiomatic Set Theory}.


225 
\newblock Dover, 1972.


226 


227 
\bibitem{takeuti87}


228 
G.~Takeuti.


229 
\newblock {\em Proof Theory}.


230 
\newblock North Holland, 2nd edition, 1987.


231 


232 
\bibitem{thompson91}


233 
Simon Thompson.


234 
\newblock {\em Type Theory and Functional Programming}.


235 
\newblock AddisonWesley, 1991.


236 


237 
\bibitem{principia}


238 
A.~N. Whitehead and B.~Russell.


239 
\newblock {\em Principia Mathematica}.

598

240 
\newblock Cambridge University Press, 1962.

104

241 
\newblock Paperback edition to *56, abridged from the 2nd edition (1927).


242 

598

243 
\bibitem{winskel93}


244 
Glynn Winskel.


245 
\newblock {\em The Formal Semantics of Programming Languages}.


246 
\newblock MIT Press, 1993.


247 

104

248 
\end{thebibliography}
