Coherence and Transitivity of Subtyping as Entailment

Giuseppe Longo (1, 2, 3) , Kathleen Milsted , Sergei Soloviev (4, 5, 6)

1 ENS-PSL - École normale supérieure - Paris
2 Département de mathématiques et d'informatique
3 La République des savoirs : Lettres, Sciences, Philosophie
4 IRIT - Institut de recherche en informatique de Toulouse
5 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
6 UT3 - Université Toulouse III - Paul Sabatier

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.

Domaines: Informatique [cs]; Mathématiques [math]

Giuseppe Longo, Kathleen Milsted, Sergei Soloviev. Coherence and Transitivity of Subtyping as Entailment. Journal of Logic and Computation, 2000, 10 (4), pp.493--526. ⟨10.1093/logcom/10.4.493⟩. ⟨hal-03318019⟩