%0 Conference Proceedings
%T A Decidable Subtyping Logic for Intersection and Union Types
%+ Logical Time for Formal Embedded System Design (KAIROS)
%A Liquori, Luigi
%A Stolze, Claude
%Z Part 3: Logic, Semantics, and Programming Theory
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B TTCS 2017 - 2nd International Conference on Topics in Theoretical Computer Science
%C Tehran, Iran
%Y Mohammad Reza Mousavi
%Y Jiří Sgall
%I Springer International Publishing
%3 Topics in Theoretical Computer Science
%V LNCS-10608
%P 74-90
%8 2017-09-12
%D 2017
%R 10.1007/978-3-319-68953-1_7
%K Subtype systems
%K Type
%K Logics and lambda-calculus
%Z Computer Science [cs]Conference papers
%X 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 $.
%G English
%Z TC 1
%Z WG 1.8
%2 https://inria.hal.science/hal-01760641/document
%2 https://inria.hal.science/hal-01760641/file/440117_1_En_7_Chapter.pdf
%L hal-01760641
%U https://inria.hal.science/hal-01760641
%~ UNICE
%~ CNRS
%~ INRIA
%~ INRIA-SOPHIA
%~ I3S
%~ INRIASO
%~ OPENAIRE
%~ INRIA_TEST
%~ LORIA2
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-TC1
%~ GENCI
%~ IFIP-WG1-8
%~ IFIP-TTCS
%~ INRIA2017
%~ UNIV-COTEDAZUR
%~ IFIP-LNCS-10608