Skip to Main content Skip to Navigation

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

Luigi Liquori 1 Claude Stolze 1
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 metadata
Contributor : Luigi Liquori Connect in order to contact the contributor
Submitted on : Friday, March 17, 2017 - 11:24:41 AM
Last modification on : Wednesday, August 11, 2021 - 12:09:51 PM
Long-term archiving on: : Sunday, June 18, 2017 - 1:00:17 PM


Files produced by the author(s)


  • HAL Id : hal-01488428, version 1



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



Record views


Files downloads