460

1 
\begin{thebibliography}{10}


2 


3 
\bibitem{andrews86}


4 
Andrews, P.~B.,


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


6 
Through Proof},


7 
\newblock Academic Press, 1986


8 


9 
\bibitem{basin91}


10 
Basin, D., Kaufmann, M.,


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


12 
\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge


13 
Univ. Press, 1991, pp.~89119


14 


15 
\bibitem{boyer86}


16 
Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.,


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


18 
\newblock {\em J. Auto. Reas. {\bf 2}}, 3 (1986), 287327


19 


20 
\bibitem{bm88book}


21 
Boyer, R.~S., Moore, J.~S.,


22 
\newblock {\em A Computational Logic Handbook},


23 
\newblock Academic Press, 1988


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{charniak80}


32 
Charniak, E., Riesbeck, C.~K., McDermott, D.~V.,


33 
\newblock {\em Artificial Intelligence Programming},


34 
\newblock Lawrence Erlbaum Associates, 1980


35 


36 
\bibitem{church40}


37 
Church, A.,


38 
\newblock A formulation of the simple theory of types,


39 
\newblock {\em J. Symb. Logic {\bf 5}\/} (1940), 5668


40 


41 
\bibitem{coen92}


42 
Coen, M.~D.,


43 
\newblock {\em Interactive Program Derivation},


44 
\newblock PhD thesis, University of Cambridge, 1992,


45 
\newblock Computer Laboratory Technical Report 272


46 


47 
\bibitem{constable86}


48 
{Constable et al.}, R.~L.,


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


50 
System},


51 
\newblock PrenticeHall, 1986


52 


53 
\bibitem{davey&priestley}


54 
Davey, B.~A., Priestley, H.~A.,


55 
\newblock {\em Introduction to Lattices and Order},


56 
\newblock Cambridge Univ. Press, 1990


57 


58 
\bibitem{dawson90}


59 
Dawson, W.~M.,


60 
\newblock {\em A Generic Logic Environment},


61 
\newblock PhD thesis, Imperial College, London, 1990


62 


63 
\bibitem{debruijn72}


64 
de~Bruijn, N.~G.,


65 
\newblock Lambda calculus notation with nameless dummies, a tool for automatic


66 
formula manipulation, with application to the {ChurchRosser Theorem},


67 
\newblock {\em Indag. Math. {\bf 34}\/} (1972), 381392


68 


69 
\bibitem{devlin79}


70 
Devlin, K.~J.,


71 
\newblock {\em Fundamentals of Contemporary Set Theory},


72 
\newblock Springer, 1979


73 


74 
\bibitem{coq}


75 
{Dowek et al.}, G.,


76 
\newblock The {Coq} proof assistant user's guide,


77 
\newblock Technical Report 134, INRIARocquencourt, 1991


78 


79 
\bibitem{dummett}


80 
Dummett, M.,


81 
\newblock {\em Elements of Intuitionism},


82 
\newblock Oxford University Press, 1977


83 


84 
\bibitem{dyckhoff}


85 
Dyckhoff, R.,


86 
\newblock Contractionfree sequent calculi for intuitionistic logic,


87 
\newblock {\em J. Symb. Logic {\bf 57}}, 3 (1992), 795807


88 


89 
\bibitem{felty91a}


90 
Felty, A.,


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


92 
proofs,


93 
\newblock In {\em Extensions of Logic Programming\/} (1991),


94 
P.~SchroederHeister, Ed., Springer, pp.~157178,


95 
\newblock LNAI 475


96 


97 
\bibitem{felty93}


98 
Felty, A.,


99 
\newblock Implementing tactics and tacticals in a higherorder logic


100 
programming language,


101 
\newblock {\em J. Auto. Reas. {\bf 11}}, 1 (1993), 4382


102 


103 
\bibitem{frost93}


104 
Frost, J.,


105 
\newblock A case study of coinduction in {Isabelle HOL},


106 
\newblock Tech. Rep. 308, Comp. Lab., Univ. Cambridge, Aug. 1993


107 


108 
\bibitem{OBJ}


109 
Futatsugi, K., Goguen, J., Jouannaud, J.P., Meseguer, J.,


110 
\newblock Principles of {OBJ2},


111 
\newblock In {\em Princ. Prog. Lang.\/} (1985), pp.~5266


112 


113 
\bibitem{gallier86}


114 
Gallier, J.~H.,


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


116 
Proving},


117 
\newblock Harper \& Row, 1986


118 


119 
\bibitem{mgordonhol}


120 
Gordon, M. J.~C., Melham, T.~F.,


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


122 
Order Logic},


123 
\newblock Cambridge Univ. Press, 1993


124 


125 
\bibitem{halmos60}


126 
Halmos, P.~R.,


127 
\newblock {\em Naive Set Theory},


128 
\newblock Van Nostrand, 1960


129 


130 
\bibitem{harperjacm}


131 
Harper, R., Honsell, F., Plotkin, G.,


132 
\newblock A framework for defining logics,


133 
\newblock {\em J.~ACM {\bf 40}}, 1 (1993), 143184


134 


135 
\bibitem{haskelltutorial}


136 
Hudak, P., Fasel, J.~H.,


137 
\newblock A gentle introduction to {Haskell},


138 
\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992)


139 


140 
\bibitem{haskellreport}


141 
Hudak, P., Jones, S.~P., Wadler, P.,


142 
\newblock Report on the programming language {Haskell}: A nonstrict, purely


143 
functional language,


144 
\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992),


145 
\newblock Version 1.2


146 


147 
\bibitem{huet75}


148 
Huet, G.~P.,


149 
\newblock A unification algorithm for typed $\lambda$calculus,


150 
\newblock {\em Theoretical Comput. Sci. {\bf 1}\/} (1975), 2757


151 


152 
\bibitem{huet78}


153 
Huet, G.~P., Lang, B.,


154 
\newblock Proving and applying program transformations expressed with


155 
secondorder patterns,


156 
\newblock {\em Acta Inf. {\bf 11}\/} (1978), 3155


157 


158 
\bibitem{mural}


159 
Jones, C.~B., Jones, K.~D., Lindsay, P.~A., Moore, R.,


160 
\newblock {\em Mural: A Formal Development Support System},


161 
\newblock Springer, 1991


162 


163 
\bibitem{alf}


164 
Magnusson, L., {Nordstr\"om}, B.,


165 
\newblock The {ALF} proof editor and its proof engine,


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


167 
'93}\/} (published 1994), Springer, pp.~213237,


168 
\newblock LNCS 806


169 


170 
\bibitem{mw81}


171 
Manna, Z., Waldinger, R.,


172 
\newblock Deductive synthesis of the unification algorithm,


173 
\newblock {\em Sci. Comput. Programming {\bf 1}}, 1 (1981), 548


174 


175 
\bibitem{martinnipkow}


176 
Martin, U., Nipkow, T.,


177 
\newblock Ordered rewriting and confluence,


178 
\newblock In {\em 10th Conf. Auto. Deduct.\/} (1990), M.~E. Stickel, Ed.,


179 
Springer, pp.~366380,


180 
\newblock LNCS 449


181 


182 
\bibitem{martinlof84}


183 
MartinL\"of, P.,


184 
\newblock {\em Intuitionistic type theory},


185 
\newblock Bibliopolis, 1984


186 


187 
\bibitem{melham89}


188 
Melham, T.~F.,


189 
\newblock Automating recursive type definitions in higher order logic,


190 
\newblock In {\em Current Trends in Hardware Verification and Automated Theorem


191 
Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,


192 
pp.~341386


193 


194 
\bibitem{millermixed}


195 
Miller, D.,


196 
\newblock Unification under a mixed prefix,


197 
\newblock {\em J. Symb. Comput. {\bf 14}}, 4 (1992), 321358


198 


199 
\bibitem{milnercoind}


200 
Milner, R., Tofte, M.,


201 
\newblock Coinduction in relational semantics,


202 
\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209220


203 


204 
\bibitem{nipkowprehofer}


205 
Nipkow, T., Prehofer, C.,


206 
\newblock Type checking type classes,


207 
\newblock In {\em 20th Princ. Prog. Lang.\/} (1993), ACM Press, pp.~409418,


208 
\newblock Revised version to appear in \bgroup\em J. Func. Prog.\egroup


209 


210 
\bibitem{noel}


211 
{No\"el}, P.,


212 
\newblock Experimenting with {Isabelle} in {ZF} set theory,


213 
\newblock {\em J. Auto. Reas. {\bf 10}}, 1 (1993), 1558


214 


215 
\bibitem{nordstrom90}


216 
{Nordstr\"om}, B., Petersson, K., Smith, J.,


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


218 
\newblock Oxford University Press, 1990


219 


220 
\bibitem{paulin92}


221 
PaulinMohring, C.,


222 
\newblock Inductive definitions in the system {Coq}: Rules and properties,


223 
\newblock Research Report 9249, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.


224 
1992


225 


226 
\bibitem{paulson85}


227 
Paulson, L.~C.,


228 
\newblock Verifying the unification algorithm in {LCF},


229 
\newblock {\em Sci. Comput. Programming {\bf 5}\/} (1985), 143170


230 


231 
\bibitem{paulson87}


232 
Paulson, L.~C.,


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


234 
\newblock Cambridge Univ. Press, 1987


235 


236 
\bibitem{paulson89}


237 
Paulson, L.~C.,


238 
\newblock The foundation of a generic theorem prover,


239 
\newblock {\em J. Auto. Reas. {\bf 5}}, 3 (1989), 363397


240 


241 
\bibitem{paulsonCOLOG}


242 
Paulson, L.~C.,


243 
\newblock A formulation of the simple theory of types (for {Isabelle}),


244 
\newblock In {\em COLOG88: International Conference on Computer Logic\/}


245 
(Tallinn, 1990), P.~MartinL\"of, G.~Mints, Eds., Estonian Academy of


246 
Sciences, Springer,


247 
\newblock LNCS 417


248 


249 
\bibitem{paulson700}


250 
Paulson, L.~C.,


251 
\newblock {Isabelle}: The next 700 theorem provers,


252 
\newblock In {\em Logic and Computer Science}, P.~Odifreddi, Ed. Academic


253 
Press, 1990, pp.~361386


254 


255 
\bibitem{paulson91}


256 
Paulson, L.~C.,


257 
\newblock {\em {ML} for the Working Programmer},


258 
\newblock Cambridge Univ. Press, 1991


259 


260 
\bibitem{paulsoncoind}


261 
Paulson, L.~C.,


262 
\newblock Coinduction and corecursion in higherorder logic,


263 
\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993


264 


265 
\bibitem{paulsonfixedpt}


266 
Paulson, L.~C.,


267 
\newblock A fixedpoint approach to implementing (co)inductive definitions,


268 
\newblock Tech. Rep. 320, Comp. Lab., Univ. Cambridge, Dec. 1993


269 


270 
\bibitem{paulsonsetI}


271 
Paulson, L.~C.,


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


273 
\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353389


274 


275 
\bibitem{paulsonsetII}


276 
Paulson, L.~C.,


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


278 
\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993


279 


280 
\bibitem{paulsonfinal}


281 
Paulson, L.~C.,


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


283 
\newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994


284 


285 
\bibitem{pelletier86}


286 
Pelletier, F.~J.,


287 
\newblock Seventyfive problems for testing automatic theorem provers,


288 
\newblock {\em J. Auto. Reas. {\bf 2}\/} (1986), 191216,


289 
\newblock Errata, JAR 4 (1988), 235236


290 


291 
\bibitem{plaisted90}


292 
Plaisted, D.~A.,


293 
\newblock A sequentstyle model elimination strategy and a positive refinement,


294 
\newblock {\em J. Auto. Reas. {\bf 6}}, 4 (1990), 389402


295 


296 
\bibitem{quaife92}


297 
Quaife, A.,


298 
\newblock Automated deduction in {von NeumannBernaysG\"odel} set theory,


299 
\newblock {\em J. Auto. Reas. {\bf 8}}, 1 (1992), 91147


300 


301 
\bibitem{sawamura92}


302 
Sawamura, H., Minami, T., Ohashi, K.,


303 
\newblock Proof methods based on sheet of thought in {EUODHILOS},


304 
\newblock Research Report IIASRR926E, International Institute for Advanced


305 
Study of Social Information Science, Fujitsu Laboratories, 1992


306 


307 
\bibitem{suppes72}


308 
Suppes, P.,


309 
\newblock {\em Axiomatic Set Theory},


310 
\newblock Dover, 1972


311 


312 
\bibitem{takeuti87}


313 
Takeuti, G.,


314 
\newblock {\em Proof Theory}, 2nd~ed.,


315 
\newblock North Holland, 1987


316 


317 
\bibitem{thompson91}


318 
Thompson, S.,


319 
\newblock {\em Type Theory and Functional Programming},


320 
\newblock AddisonWesley, 1991


321 


322 
\bibitem{principia}


323 
Whitehead, A.~N., Russell, B.,


324 
\newblock {\em Principia Mathematica},


325 
\newblock Cambridge Univ. Press, 1962,


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


327 


328 
\bibitem{wosbledsoe}


329 
Wos, L.,


330 
\newblock Automated reasoning and {Bledsoe's} dream for the field,


331 
\newblock In {\em Automated Reasoning: Essays in Honor of {Woody Bledsoe}},


332 
R.~S. Boyer, Ed. Kluwer Academic Publishers, 1991, pp.~297342


333 


334 
\end{thebibliography}
