The ``relevance of intersection and union types

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

zbMATH Keywords

union typesfragment of intuitionistic logicextension of type theory for combinatorsHilbert style logic

Mathematics Subject Classification ID

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