References

[And86]

Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Computer Science and Applied Mathematics. Academic Press, 1986.

[Bar84]

Henk P. Barendregt. The Lambda Calculus, Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, Amsterdam, revised edition, 1984.

[DW85]

Martin D. Davis and Elaine J. Weyuker. Computability, Complexity and Languages. Academic Press, New York, 1985.

[Dyc92]

Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57(3):795--807, 1992.

[GLT89]

Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Hue73]

Gérard P. Huet. A mechanization of type theory. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence, pages 139--146, Stanford University, Stanford, California, August 1973.

[Hue75]

Gérard P. Huet. A unification algorithm for typed l-calculus. Theoretical Computer Science, 1:27--57, 1975.

[Joh92]

Peter T. Johnstone. Notes on Logic and Set Theory. Cambridge University Press, 1992.

[Kle67]

Stephen Cole Kleene. Mathematical Logic. John Wiley and Sons, 1967.

[Koh95]

Michael Kohlhase. Higher-order tableaux. In Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 1995.

[Man77]

Youri I. Manin. A Course in Mathematical Logic. Graduate Texts in Mathematics. Springer Verlag, 1977.

[Mil87]

Dale A. Miller. A compact representation of proofs. Studia Logica, 46(4), 1987.

[MMO93]

Pierangelo Miglioli, Ugo Moscato, and Mario Ornaghi. How to avoid duplications in refutation systems for intuitionistic and Kuroda logic. In Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 1993.

[Rob66]

Abraham Robinson. Non-standard Analysis. Studies in logic and the foundations of mathematics. Amsterdam, North-Holland Pub. Co., 1966.

[Sch77]

Helmut Schwichtenberg. Proof theory: Some applications of cut-elimination. In Jon Barwise, editor, Handbook of Mathematical Logic, chapter D.2, pages 867--895. North-Holland Publishing Company, 1977.

[SG89]

W. Snyder and J. Gallier. Higher order unification revisited: Complete sets of tranformations. Journal of Symbolic Computation, 8(1 & 2):101--140, 1989. Special issue on unification. Part two. Available at ftp://ftp.cis.upenn.edu/pub/papers/gallier/hounif.dvi.Z.

[Sho67]

Joseph R. Shoenfield. Mathematical Logic. Addison Wesley, 1967.

[SS89]

Manfred Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations, volume 395 of Lecture Notes in Artificial Intelligence. Springer Verlag, 1989.

[Wal88]

Christoph Walther. Many-sorted unification. Journal of the ACM, 35(1):1--17, 1988.