A logic of subtyping
G. Loop, Kathleen Milsted, S. Soloviev · 2002
The relation of inclusion between types has been suggested by the practice of programming, as it enriches the polymorphism of functional languages. We propose a simple (and linear) calculus of sequents for subtyping as logical entailment. This allows to derive a complete and coherent approach to subtyping from a few, logically meaningful, sequents. In particular, transitivity and anti-symmetry are derived from elementary logical principles, which stresses the power of sequents and Gentzen-style proof methods. Indeed, proof techniques based on cut-elimination are at the core of our results.