The ``relevance of intersection and union types
From MaRDI portal
Publication:1381437
DOI10.1305/NDJFL/1039724889zbMath0918.03008OpenAlexW1969658529MaRDI QIDQ1381437
Betti Venneri, Silvia Ghilezan, Mariangiola Dezani-Ciancaglini
Publication date: 17 August 1999
Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1305/ndjfl/1039724889
union typesfragment of intuitionistic logicextension of type theory for combinatorsHilbert style logic
Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)
Related Items (8)
A Realizability Interpretation for Intersection and Union Types ⋮ A binary modal logic for the intersection types of lambda-calculus. ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca ⋮ A typed lambda calculus with intersection types ⋮ Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage ⋮ Full intersection types and topologies in lambda calculus ⋮ Inhabitation of Low-Rank Intersection Types ⋮ The Relevance of Semantic Subtyping
Cites Work
- Combinatory logic. With two sections by William Craig.
- Coppo-Dezani types do not correspond to propositional logic
- The completeness of provable realizability
- Domain theory in logical form
- Intersection types for combinatory logic
- The semantics of entailment. III
- Type inference, abstract interpretation and strictness analysis
- Proof-functional connectives and realizability
- Intersection and union types: Syntax and semantics
- A propositional calculus with denumerable matrix
- Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
- An ideal model for recursive polymorphic types
- Functional Characters of Solvable Terms
- Intersection Types as Logical Formulae
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: The ``relevance of intersection and union types