A Decidable Subtyping Logic for Intersection and Union Types - Archive ouverte HAL Access content directly
Conference Papers Year : 2017

## A Decidable Subtyping Logic for Intersection and Union Types

(1) , (1)
1
Luigi Liquori
Claude Stolze
• Function : Author
• PersonId : 1012502

#### 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$ .

#### Domains

Computer Science [cs]

### Dates and versions

hal-01760641 , version 1 (06-04-2018)

### Licence

Attribution - CC BY 4.0

### Identifiers

• HAL Id : hal-01760641 , version 1
• DOI :

### Cite

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⟩

### Export

BibTeX TEI Dublin Core DC Terms EndNote Datacite

288 View