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

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 :
Rapport
[Research Report] Inria. 2017
Liste complète des métadonnées

https://hal.inria.fr/hal-01488428
Contributeur : Luigi Liquori <>
Soumis le : vendredi 17 mars 2017 - 11:24:41
Dernière modification le : jeudi 11 janvier 2018 - 16:38:53
Document(s) archivé(s) le : dimanche 18 juin 2017 - 13:00:17

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01488428, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

345

Téléchargements de fichiers

34