A Decidable Subtyping Logic for Intersection and Union Types

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. Using the proof-as-types and terms-as-propositions paradigms, we extend the proof-functional logic previously defined by the authors with a decidable subtyping relation and we show the extension to be isomorphic to the Barbanera-Dezani-de'Liguoro type assignment system: we also provide a sound interpretation of the proof-functional logic using Mints' realizers. We present a decidable algorithm for subtyping in presence of intersection and union types. The algorithm is presented in declarative style, and it is conceived to work for the minimal (sub)type theory $Ξ$ of the above type assignment system: it is proved to be sound and complete.
Type de document :
Communication dans un congrès
Topics in Theoretical Computer Science, TTCS 2017, Sep 2017, Teheran, Iran. Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [47 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01560681
Contributeur : Luigi Liquori <>
Soumis le : mardi 11 juillet 2017 - 19:42:53
Dernière modification le : jeudi 11 janvier 2018 - 16:48:52

Fichier

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

Identifiants

  • HAL Id : hal-01560681, version 1

Collections

Citation

Luigi Liquori, Claude Stolze. A Decidable Subtyping Logic for Intersection and Union Types. Topics in Theoretical Computer Science, TTCS 2017, Sep 2017, Teheran, Iran. Lecture Notes in Computer Science. 〈hal-01560681〉

Partager

Métriques

Consultations de la notice

75

Téléchargements de fichiers

27