We present two complete systems for subtyping polymorphic types. One system is in the style of natural deduction, while another is a Gentzen style sequent calculus system. We prove several metamathematical properties for these systems including cut elimination, subject reduction, coherence, and decidability of type reconstruction. Following the approach by J.Mitchell, the sequents are given a simple semantics using logical relations over applicative structures. The systems are complete with respect to this semantics. The logic which emerges from this paper can be seen as a successor to the original Hilbert style system proposed by J. Mitchell in 1988, and to the “half way” sequent calculus of G. Longo, K. Milsted and S. Soloviev proposed in 1995.
CITATION STYLE
Tiuryn, J. (1996). A sequent calculus for subtyping polymorphic types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1113, pp. 135–155). Springer Verlag. https://doi.org/10.1007/3-540-61550-4_144
Mendeley helps you to discover research relevant for your work.