Home  Online Resources  Table of Contents

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: longo@dmi.ens.fr, 2NET, France Télécom, 28 chemin du Vieux Chêne, BP 98, 38243 Meylan Cedex, France, E-mail: kathleen.milsted@cnet.francetelecom.fr, 3IRIT, Université de Toulouse-III, 118 route de Narbonne, 31062 Toulouse, France, E-mail: soloviev@irit.fr

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

  Full-Text PDF  (327 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2000.