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
Abstract: 
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

SCOPUSTM   
Citations

24
checked on Jan 29, 2023

Page view(s)

20
checked on Jan 30, 2023

Google ScholarTM

Check

Altmetric

Altmetric


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