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


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


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.

114

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


20 


21 
\bibitem{camilleri92}


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


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


24 
prover.


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


26 
August 1992.

104

27 


28 
\bibitem{church40}


29 
Alonzo Church.


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


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


32 


33 
\bibitem{dummett}


34 
Michael Dummett.


35 
\newblock {\em Elements of Intuitionism}.

114

36 
\newblock Oxford University Press, 1977.

104

37 


38 
\bibitem{dyckhoff}


39 
Roy Dyckhoff.


40 
\newblock Contractionfree sequent calculi for intuitionistic logic.


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


42 


43 
\bibitem{felty91a}


44 
Amy Felty.


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


46 
proofs.


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


48 
Programming}, pages 157178. Springer, 1991.


49 
\newblock LNAI 475.


50 

114

51 
\bibitem{frost93}


52 
Jacob Frost.


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


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


55 
August 1993.


56 

104

57 
\bibitem{OBJ}


58 
K.~Futatsugi, J.A. Goguen, JeanPierre Jouannaud, and J.~Meseguer.


59 
\newblock Principles of {OBJ2}.


60 
\newblock In {\em Symposium on Principles of Programming Languages}, pages


61 
5266, 1985.


62 


63 
\bibitem{gallier86}


64 
J.~H. Gallier.


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


66 
Proving}.


67 
\newblock Harper \& Row, 1986.


68 

114

69 
\bibitem{mgordon88a}

104

70 
Michael J.~C. Gordon.


71 
\newblock {HOL}: A proof generating system for higherorder logic.


72 
\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em {VLSI}


73 
Specification, Verification and Synthesis}, pages 73128. Kluwer Academic


74 
Publishers, 1988.


75 


76 
\bibitem{halmos60}


77 
Paul~R. Halmos.


78 
\newblock {\em Naive Set Theory}.


79 
\newblock Van Nostrand, 1960.


80 


81 
\bibitem{huet78}


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


83 
\newblock Proving and applying program transformations expressed with


84 
secondorder patterns.


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


86 

114

87 
\bibitem{mw81}


88 
Zohar Manna and Richard Waldinger.


89 
\newblock Deductive synthesis of the unification algorithm.


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


91 

104

92 
\bibitem{martinlof84}


93 
Per MartinL\"of.


94 
\newblock {\em Intuitionistic type theory}.


95 
\newblock Bibliopolis, 1984.


96 

114

97 
\bibitem{milnercoind}


98 
Robin Milner and Mads Tofte.


99 
\newblock Coinduction in relational semantics.


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

104

101 


102 
\bibitem{noel}


103 
Philippe {No\"el}.


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

114

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

104

106 


107 
\bibitem{nordstrom90}


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


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

114

110 
\newblock Oxford University Press, 1990.


111 


112 
\bibitem{paulin92}


113 
Christine PaulinMohring.


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


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


116 
December 1992.


117 


118 
\bibitem{paulsonsetI}


119 
Lawrence~C. Paulson.


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


121 
\newblock {\em Journal of Automated Reasoning}.


122 
\newblock In press; draft available as Report 271, University of Cambridge


123 
Computer Laboratory.


124 


125 
\bibitem{paulson85}


126 
Lawrence~C. Paulson.


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


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

104

129 


130 
\bibitem{paulson87}


131 
Lawrence~C. Paulson.


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


133 
\newblock Cambridge University Press, 1987.


134 


135 
\bibitem{paulsonCOLOG}


136 
Lawrence~C. Paulson.


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


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


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


140 
of Sciences, Springer.


141 
\newblock LNCS 417.


142 

114

143 
\bibitem{paulson91}


144 
Lawrence~C. Paulson.


145 
\newblock {\em {ML} for the Working Programmer}.


146 
\newblock Cambridge University Press, 1991.


147 


148 
\bibitem{paulsoncoind}


149 
Lawrence~C. Paulson.


150 
\newblock Coinduction and corecursion in higherorder logic.


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


152 
July 1993.


153 


154 
\bibitem{paulsonfixedpt}


155 
Lawrence~C. Paulson.


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


157 
\newblock Technical report, University of Cambridge Computer Laboratory, 1993.


158 
\newblock Draft.


159 


160 
\bibitem{paulsonsetII}


161 
Lawrence~C. Paulson.


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


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


164 
1993.


165 

104

166 
\bibitem{pelletier86}


167 
F.~J. Pelletier.


168 
\newblock Seventyfive problems for testing automatic theorem provers.


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


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


171 


172 
\bibitem{plaisted90}


173 
David~A. Plaisted.


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


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


176 


177 
\bibitem{quaife92}


178 
Art Quaife.


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


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


181 


182 
\bibitem{suppes72}


183 
Patrick Suppes.


184 
\newblock {\em Axiomatic Set Theory}.


185 
\newblock Dover, 1972.


186 


187 
\bibitem{takeuti87}


188 
G.~Takeuti.


189 
\newblock {\em Proof Theory}.


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


191 


192 
\bibitem{thompson91}


193 
Simon Thompson.


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


195 
\newblock AddisonWesley, 1991.


196 


197 
\bibitem{principia}


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


199 
\newblock {\em Principia Mathematica}.


200 
\newblock Cambridge University Press, 1962.


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


202 


203 
\end{thebibliography}
