The ``relevance'' of intersection and union types
type: Item
instance of: scholarly article
title: The ``relevance'' of intersection and union types
zbMATH Open document ID: 0918.03008
author: Mariangiola Dezani-Ciancaglini
author: Silvia Ghilezan
author: Betti Venneri
published in: Notre Dame Journal of Formal Logic
publication date: 1999-08-17T00:00:00Z
review text: It is well known that the (simple \(\to\)) types of combinators are exactly the theorems of intuitionistic implicational logic. In the extended \(\to\wedge\) type theory all combinators with normal forms have types, but these types form a Hilbert-style logic, discovered by Venneri, related to the Meyer-Routley minimal logic \(B^+\), that is a proper sublogic of the \(\to\wedge\) fragment of intuitionistic logic. This paper examines the logic that corresponds to a further extension of type theory for combinators, that also includes union types. The Hilbert style logic obtained is again related to Meyer and Routley's \(B^+\), but while its \(\to\wedge\) fragment remains a sublogic of the \(\to\wedge\) fragment of intuitionistic logic, surprisingly the full \(\to\wedge\vee\) logic obtained from the type theory is not a sublogic of intuitionistic logic.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B20
zbMATH DE Number: 1129583
zbMATH Keywords: extension of type theory for combinators
zbMATH Keywords: union types
zbMATH Keywords: Hilbert style logic
zbMATH Keywords: fragment of intuitionistic logic
reviewed by: Martin W. Bunder
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1305/ndjfl/1039724889
OpenAlex ID: W1969658529
cites work: Domain theory in logical form
cites work: Q4035227
cites work: Intersection and union types: Syntax and semantics
cites work: Proof-functional connectives and realizability
cites work: Functional Characters of Solvable Terms
cites work: Type inference, abstract interpretation and strictness analysis
cites work: Combinatory logic. With two sections by William Craig.
cites work: Intersection types for combinatory logic
cites work: A propositional calculus with denumerable matrix
cites work: Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
cites work: Coppo-Dezani types do not correspond to propositional logic
cites work: Q4722037
cites work: Q4723730
cites work: An ideal model for recursive polymorphic types
cites work: Q4103076
cites work: The semantics of entailment. III
cites work: The completeness of provable realizability
cites work: Intersection Types as Logical Formulae
DOI: 10.1305/NDJFL/1039724889
Recommended article: The Duality of Classical Intersection and Union Types
Recommended article: Q4993854
Recommended article: Elaborating intersection and union types
Recommended article: Intersection and union types: Syntax and semantics
Recommended article: Intersection and union types
Recommended article: Q5369484
Recommended article: Intersection, Universally Quantified, and Reference Types
Recommended article: A Realizability Interpretation for Intersection and Union Types
Recommended article: Preciseness of Subtyping on Intersection and Union Types
description: scientific article; zbMATH DE number 1129583