A Decidable Subtyping Logic for Intersection and Union Types (full version) - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2017

A Decidable Subtyping Logic for Intersection and Union Types (full version)

(1) , (1)
1

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. We present a proof-functional logic and we give a semantics using Mints' realizers accounting for intersection types, union types, and subtyping. The semantics interprets the type ω as the set universe, the → type as a function space, the ∩ and ∪ types as set intersection and set union, respectively, and the subtype relation as a subset operator. Using the proof-as-types and terms-as-propositions paradigms, we extend the typed calculus previously defined by the authors with a decidable subtyping relation and we show this calculus to be isomorphic to the Barbanera-Dezani-Ciancaglini-de'Liguoro type assignment system. A subtyping algorithm is presented and proved to be sound and complete. Hindley gave a subtyping algorithm for intersection types but, as far as we know, there is no system in the literature also including union types.
Fichier principal
Vignette du fichier
paper.pdf (371.52 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01488428 , version 1 (17-03-2017)

Identifiers

  • HAL Id : hal-01488428 , version 1

Cite

Luigi Liquori, Claude Stolze. A Decidable Subtyping Logic for Intersection and Union Types (full version). [Research Report] Inria. 2017. ⟨hal-01488428⟩
285 View
325 Download

Share

Gmail Facebook Twitter LinkedIn More