104

1 
\begin{thebibliography}{10}


2 


3 
\bibitem{andrews86}


4 
Peter~B. Andrews.


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


6 
Through Proof}.


7 
\newblock Academic Press, 1986.


8 

114

9 
\bibitem{basin91}


10 
David Basin and Matt Kaufmann.


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


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

359

13 
Frameworks}, pages 89119. 1991.

114

14 

104

15 
\bibitem{boyer86}


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


17 
Lawrence Wos.


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

359

19 
\newblock 2(3):287327, 1986.

114

20 


21 
\bibitem{camilleri92}


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


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


24 
prover.

359

25 
\newblock Technical Report 265, August 1992.

104

26 


27 
\bibitem{church40}


28 
Alonzo Church.


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

359

30 
\newblock 5:5668, 1940.


31 


32 
\bibitem{coen92}


33 
Martin~D. Coen.


34 
\newblock {\em Interactive Program Derivation}.


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


36 
\newblock Computer Laboratory Technical Report 272.


37 


38 
\bibitem{constable86}


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


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


41 
System}.


42 
\newblock 1986.


43 


44 
\bibitem{davey&priestley}


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


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


47 
\newblock 1990.


48 


49 
\bibitem{devlin79}


50 
Keith~J. Devlin.


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


52 
\newblock Springer, 1979.

104

53 


54 
\bibitem{dummett}


55 
Michael Dummett.


56 
\newblock {\em Elements of Intuitionism}.

114

57 
\newblock Oxford University Press, 1977.

104

58 


59 
\bibitem{dyckhoff}


60 
Roy Dyckhoff.


61 
\newblock Contractionfree sequent calculi for intuitionistic logic.

359

62 
\newblock 57(3):795807, 1992.

104

63 


64 
\bibitem{felty91a}


65 
Amy Felty.


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


67 
proofs.


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


69 
Programming}, pages 157178. Springer, 1991.


70 
\newblock LNAI 475.


71 

114

72 
\bibitem{frost93}


73 
Jacob Frost.


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

359

75 
\newblock Technical Report 308, August 1993.

104

76 


77 
\bibitem{gallier86}


78 
J.~H. Gallier.


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


80 
Proving}.


81 
\newblock Harper \& Row, 1986.


82 

359

83 
\bibitem{mgordonhol}


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


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


86 
Order Logic}.


87 
\newblock 1993.

104

88 


89 
\bibitem{halmos60}


90 
Paul~R. Halmos.


91 
\newblock {\em Naive Set Theory}.


92 
\newblock Van Nostrand, 1960.


93 


94 
\bibitem{huet78}


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


96 
\newblock Proving and applying program transformations expressed with


97 
secondorder patterns.


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


99 

359

100 
\bibitem{alf}


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


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


103 
\newblock In {\em : International Workshop {TYPES '93}}, pages 213237.


104 
Springer, published 1994.


105 
\newblock LNCS 806.


106 

114

107 
\bibitem{mw81}


108 
Zohar Manna and Richard Waldinger.


109 
\newblock Deductive synthesis of the unification algorithm.


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


111 

104

112 
\bibitem{martinlof84}


113 
Per MartinL\"of.


114 
\newblock {\em Intuitionistic type theory}.


115 
\newblock Bibliopolis, 1984.


116 

359

117 
\bibitem{melham89}


118 
Thomas~F. Melham.


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


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


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


122 
341386. Springer, 1989.


123 

114

124 
\bibitem{milnercoind}


125 
Robin Milner and Mads Tofte.


126 
\newblock Coinduction in relational semantics.


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

104

128 


129 
\bibitem{noel}


130 
Philippe {No\"el}.


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

359

132 
\newblock 10(1):1558, 1993.

104

133 


134 
\bibitem{nordstrom90}


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


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

114

137 
\newblock Oxford University Press, 1990.


138 


139 
\bibitem{paulin92}


140 
Christine PaulinMohring.


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


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


143 
December 1992.


144 


145 
\bibitem{paulson85}


146 
Lawrence~C. Paulson.


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


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

104

149 


150 
\bibitem{paulson87}


151 
Lawrence~C. Paulson.


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

359

153 
\newblock 1987.

104

154 


155 
\bibitem{paulsonCOLOG}


156 
Lawrence~C. Paulson.


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


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


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


160 
of Sciences, Springer.


161 
\newblock LNCS 417.


162 

114

163 
\bibitem{paulsoncoind}


164 
Lawrence~C. Paulson.


165 
\newblock Coinduction and corecursion in higherorder logic.

359

166 
\newblock Technical Report 304, July 1993.

114

167 


168 
\bibitem{paulsonfixedpt}


169 
Lawrence~C. Paulson.

359

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


171 
\newblock Technical Report 320, December 1993.


172 


173 
\bibitem{paulsonsetI}


174 
Lawrence~C. Paulson.


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


176 
\newblock 11(3):353389, 1993.

114

177 


178 
\bibitem{paulsonsetII}


179 
Lawrence~C. Paulson.


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

359

181 
\newblock Technical Report 312, 1993.


182 


183 
\bibitem{paulsonfinal}


184 
Lawrence~C. Paulson.


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


186 
\newblock Technical report, 1994.

114

187 

104

188 
\bibitem{pelletier86}


189 
F.~J. Pelletier.


190 
\newblock Seventyfive problems for testing automatic theorem provers.

359

191 
\newblock 2:191216, 1986.

104

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


193 


194 
\bibitem{plaisted90}


195 
David~A. Plaisted.


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

359

197 
\newblock 6(4):389402, 1990.

104

198 


199 
\bibitem{quaife92}


200 
Art Quaife.


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

359

202 
\newblock 8(1):91147, 1992.

104

203 


204 
\bibitem{suppes72}


205 
Patrick Suppes.


206 
\newblock {\em Axiomatic Set Theory}.


207 
\newblock Dover, 1972.


208 


209 
\bibitem{takeuti87}


210 
G.~Takeuti.


211 
\newblock {\em Proof Theory}.


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


213 


214 
\bibitem{thompson91}


215 
Simon Thompson.


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


217 
\newblock AddisonWesley, 1991.


218 


219 
\bibitem{principia}


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


221 
\newblock {\em Principia Mathematica}.

359

222 
\newblock 1962.

104

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


224 


225 
\end{thebibliography}
