Subtyping Relations as Sequents
In this talk, I'll present a work-in-progress study on the logical content of the subtyping relation, in presence of different type operators. A sequent calculus for the subtyping with the arrow operator and the universal quantifier has been extensively studied by J. Tiuryn (MFCS'96 proocedings). Indipendently (but with much more naive tools) I studied a similar sequent calculus for arrow plus intersection type operators (Master Thesis, 1993). At the moment, we are studying a subtyping relation with the cartesian product as a type operator, and the ultimate goal should be the integration of all the calculi in a unified framework calculus. This is joint work with Jerzy Tiuryn, University of Warsaw.