A Decidable Subtyping Logic for Intersection and Union Types

Luigi Liquori 1 Claude Stolze 1
1 KAIROS - Logical Time for Formal Embedded System Design
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : Using Curry-Howard isomorphism, we extend the typed lambda-calculus with intersection and union types, and its corresponding proof-functional logic, previously defined by the authors, with subtyping and explicit coercions.We show the extension of the lambda-calculus to be isomorphic to the Barbanera-Dezani-de’Liguoro type assignment system and we provide a sound interpretation of the proof-functional logic with the $\mathsf {NJ}(\beta )$ logic, using Mints’ realizers.We finally present a sound and complete algorithm for subtyping in presence of intersection and union types. The algorithm is conceived to work for the (sub)type theory $\varXi $ .
Type de document :
Communication dans un congrès
Mohammad Reza Mousavi; Jiří Sgall. TTCS 2017 - 2nd International Conference on Topics in Theoretical Computer Science, Sep 2017, Tehran, Iran. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10608, pp.74-90, 2017, Topics in Theoretical Computer Science. 〈10.1007/978-3-319-68953-1_7〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01760641
Contributeur : Hal Ifip <>
Soumis le : vendredi 6 avril 2018 - 15:08:02
Dernière modification le : mardi 24 avril 2018 - 17:25:45

Fichier

 Accès restreint
Fichier visible le : 2020-01-01

Connectez-vous pour demander l'accès au fichier

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Luigi Liquori, Claude Stolze. A Decidable Subtyping Logic for Intersection and Union Types. Mohammad Reza Mousavi; Jiří Sgall. TTCS 2017 - 2nd International Conference on Topics in Theoretical Computer Science, Sep 2017, Tehran, Iran. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10608, pp.74-90, 2017, Topics in Theoretical Computer Science. 〈10.1007/978-3-319-68953-1_7〉. 〈hal-01760641〉

Partager

Métriques

Consultations de la notice

185