A sequent calculus for subtyping polymorphic types

We present two complete systems for polymorphic types with subtyping. One s ystem is in the style of natural deduction, while another is a Gentzen-styl e 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 ap plicative structures. The systems are complete with respect to this semanti cs. The logic which emerges from this paper can be seen as a successor to t he original Hilbert style system proposed by J. Mitchell in 1988, and to th e "half way" sequent calculus of G. Longo, K. Milsted, and S. Soloviev prop osed in 1995. (C) 2001 Academic Press.