Journal of Logic and Computation, Volume 10, Issue 4, pp. 493-526: Abstract.
Coherence and transitivity of subtyping as entailment
G Longo1, K Milsted2 and S Soloviev3
1LIENS(CNRS) and DMI, Ecole Normale Supérieure, 45 rue d'Ulm, 75005 Paris, France, E-mail: email@example.com, 2NET, France Télécom, 28 chemin du Vieux Chêne, BP 98, 38243 Meylan Cedex, France, E-mail: firstname.lastname@example.org, 3IRIT, Université de Toulouse-III, 118 route de Narbonne, 31062 Toulouse, France, E-mail: email@example.com
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) sequent calculus for subtyping as logical entailment. This allows us to derive a complete and coherent approach to subtyping from a few, logically meaningful sequents. In particular, transitivity and anti-symmetry will be derived from elementary logical principles.
Keywords: second-order logic, Gentzen sequent calculus, polymorphism, coercive subtyping, cut-elimination