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 


9 
\bibitem{boyer86}


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


11 
Lawrence Wos.


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


13 
\newblock {\em Journal of Automated Reasoning}, 2:287327, 1986.


14 


15 
\bibitem{church40}


16 
Alonzo Church.


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


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


19 


20 
\bibitem{dummett}


21 
Michael Dummett.


22 
\newblock {\em Elements of Intuitionism}.


23 
\newblock Oxford, 1977.


24 


25 
\bibitem{dyckhoff}


26 
Roy Dyckhoff.


27 
\newblock Contractionfree sequent calculi for intuitionistic logic.


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


29 


30 
\bibitem{felty91a}


31 
Amy Felty.


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


33 
proofs.


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


35 
Programming}, pages 157178. Springer, 1991.


36 
\newblock LNAI 475.


37 


38 
\bibitem{OBJ}


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


40 
\newblock Principles of {OBJ2}.


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


42 
5266, 1985.


43 


44 
\bibitem{gallier86}


45 
J.~H. Gallier.


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


47 
Proving}.


48 
\newblock Harper \& Row, 1986.


49 


50 
\bibitem{gordon88a}


51 
Michael J.~C. Gordon.


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


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


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


55 
Publishers, 1988.


56 


57 
\bibitem{halmos60}


58 
Paul~R. Halmos.


59 
\newblock {\em Naive Set Theory}.


60 
\newblock Van Nostrand, 1960.


61 


62 
\bibitem{huet78}


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


64 
\newblock Proving and applying program transformations expressed with


65 
secondorder patterns.


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


67 


68 
\bibitem{martinlof84}


69 
Per MartinL\"of.


70 
\newblock {\em Intuitionistic type theory}.


71 
\newblock Bibliopolis, 1984.


72 


73 
\bibitem{nipkowprehofer}


74 
Tobias Nipkow and Christian Prehofer.


75 
\newblock Type checking type classes.


76 
\newblock In {\em 20th ACM Symp.\ Principles of Programming Languages}, 1993.


77 
\newblock To appear.


78 


79 
\bibitem{noel}


80 
Philippe {No\"el}.


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


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


83 
\newblock In press.


84 


85 
\bibitem{nordstrom90}


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


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


88 
\newblock Oxford, 1990.


89 


90 
\bibitem{paulson87}


91 
Lawrence~C. Paulson.


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


93 
\newblock Cambridge University Press, 1987.


94 


95 
\bibitem{paulsonCOLOG}


96 
Lawrence~C. Paulson.


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


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


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


100 
of Sciences, Springer.


101 
\newblock LNCS 417.


102 


103 
\bibitem{pelletier86}


104 
F.~J. Pelletier.


105 
\newblock Seventyfive problems for testing automatic theorem provers.


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


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


108 


109 
\bibitem{plaisted90}


110 
David~A. Plaisted.


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


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


113 


114 
\bibitem{quaife92}


115 
Art Quaife.


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


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


118 


119 
\bibitem{suppes72}


120 
Patrick Suppes.


121 
\newblock {\em Axiomatic Set Theory}.


122 
\newblock Dover, 1972.


123 


124 
\bibitem{takeuti87}


125 
G.~Takeuti.


126 
\newblock {\em Proof Theory}.


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


128 


129 
\bibitem{thompson91}


130 
Simon Thompson.


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


132 
\newblock AddisonWesley, 1991.


133 


134 
\bibitem{principia}


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


136 
\newblock {\em Principia Mathematica}.


137 
\newblock Cambridge University Press, 1962.


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


139 


140 
\end{thebibliography}
