Skip to Main content Skip to Navigation
Conference papers

A Decidable Subtyping Logic for Intersection and Union Types

Luigi Liquori 1 Claude Stolze 1
1 KAIROS - Logical Time for Formal Embedded System Design
Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués, CRISAM - Inria Sophia Antipolis - Méditerranée
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 $ .
Document type :
Conference papers
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, April 6, 2018 - 3:08:02 PM
Last modification on : Thursday, May 20, 2021 - 9:20:01 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Luigi Liquori, Claude Stolze. A Decidable Subtyping Logic for Intersection and Union Types. TTCS 2017 - 2nd International Conference on Topics in Theoretical Computer Science, Sep 2017, Tehran, Iran. pp.74-90, ⟨10.1007/978-3-319-68953-1_7⟩. ⟨hal-01760641⟩



Record views


Files downloads