Coercive subtyping: Theory and implementation

Zhaohui Luo (1) , Sergei Soloviev (2, 3) , Tao Xue (1)

1 Department of Computer Science
2 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
3 ITMO - National Research University of Information Technologies, Mechanics and Optics [St. Petersburg]

Coercive subtyping is a useful and powerful framework of subtyping for type theories. The key idea of coercive subtyping is subtyping as abbreviation. In this paper, we give a new and adequate formulation of T[C], the system that extends a type theory T with coercive subtyping based on a set C of basic subtyping judgements, and show that coercive subtyping is a conservative extension and, in a more general sense, a definitional extension. We introduce an intermediate system, the star-calculus T[C]^@?, in which the positions that require coercion insertions are marked, and show that T[C]^@? is a conservative extension of T and that T[C]^@? is equivalent to T[C]. This makes clear what we mean by coercive subtyping being a conservative extension, on the one hand, and amends a technical problem that has led to a gap in the earlier conservativity proof, on the other. We also compare coercive subtyping with the 'ordinary' notion of subtyping - subsumptive subtyping, and show that the former is adequate for type theories with canonical objects while the latter is not. An improved implementation of coercive subtyping is done in the proof assistant Plastic.

Mots clés: Conservativity; Coercive subtyping; Definitional extension; Subsumptive subtyping; Type theory

Domaines: Génie logiciel [cs.SE]; Architectures Matérielles [cs.AR]; Cryptographie et sécurité [cs.CR]; Systèmes embarqués; Interface homme-machine [cs.HC]; Modélisation et simulation

Zhaohui Luo, Sergei Soloviev, Tao Xue. Coercive subtyping: Theory and implementation. Information and Computation, 2013, vol. 223, pp.18-42. ⟨10.1016/j.ic.2012.10.020⟩. ⟨hal-01130574⟩