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

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

https://hal.inria.fr/hal-01488428
Contributor : Luigi Liquori <>
Submitted on : Friday, March 17, 2017 - 11:24:41 AM
Last modification on : Wednesday, March 13, 2019 - 1:21:35 AM
Long-term archiving on : Sunday, June 18, 2017 - 1:00:17 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01488428, version 1

Collections

Citation

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

Share

Metrics

Record views

421

Files downloads

281