Authors: Dezani-Ciancaglini, Mariangiola
Ghilezan, Silvia 
Venneri, Betti
Title: The “Relevance” of intersection and union types
Journal: Notre Dame Journal of Formal Logic
Volume: 38
Issue: 2
First page: 246
Last page: 269
Issue Date: 1-Jan-1997
ISSN: 0029-4527
DOI: 10.1305/ndjfl/1039724889
The aim of this paper is to investigate a Curry-Howard interpretation of the intersection and union type inference system for Combinatory Logic. Types are interpreted as formulas of a Hilbert-style logic L, which turns out to be an extension of the intuitionistic logic with respect to provable disjunctive formulas (because of new equivalence relations on formulas), while the implicational-conjunctive fragment of L is still a fragment of intuitionisticlogic. Moreover, typable terms are translated in a typed version, so that ∨-∧-typed combinatory logic terms are proved to completely codify the associated logical proofs.
Publisher: University of Notre Dame

Show full item record


checked on May 18, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.