A Decidable Subtyping Logic for Intersection and Union Types (full version)

Luigi Liquori 1, 2 Claude Stolze 1, 2
1 KAIROS - Logical Time for Formal Embedded System Design
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : Proof-functional logical connectives allow reasoning about the structure of logical proofs, in this way giving to the latter the status of first-class objects. This is in contrast to classical truth-functional connectives where the meaning of a compound formula is dependent only on the truth value of its subformulas. We present a proof-functional logic and we give a semantics using Mints' realizers accounting for intersection types, union types, and subtyping. The semantics interprets the type ω as the set universe, the → type as a function space, the ∩ and ∪ types as set intersection and set union, respectively, and the subtype relation as a subset operator. Using the proof-as-types and terms-as-propositions paradigms, we extend the typed calculus previously defined by the authors with a decidable subtyping relation and we show this calculus to be isomorphic to the Barbanera-Dezani-Ciancaglini-de'Liguoro type assignment system. A subtyping algorithm is presented and proved to be sound and complete. Hindley gave a subtyping algorithm for intersection types but, as far as we know, there is no system in the literature also including union types.
Type de document :
[Research Report] Inria. 2017
Liste complète des métadonnées

Contributeur : Luigi Liquori <>
Soumis le : vendredi 17 mars 2017 - 11:24:41
Dernière modification le : mercredi 13 mars 2019 - 01:21:35
Document(s) archivé(s) le : dimanche 18 juin 2017 - 13:00:17


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01488428, version 1



Luigi Liquori, Claude Stolze. A Decidable Subtyping Logic for Intersection and Union Types (full version). [Research Report] Inria. 2017. 〈hal-01488428〉



Consultations de la notice


Téléchargements de fichiers