The "Relevance" of Intersection and Union Types

Notre Dame Journal of Formal Logic 38 (2):246-269 (1997)
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 intuitionistic logic. Moreover, typable terms are translated in a typed version, so that --typed combinatory logic terms are proved to completely codify the associated logical proofs
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1305/ndjfl/1039724889
Options
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history
Request removal from index
Download options
Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 28,191
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles
Strong Normalization and Typability with Intersection Types.Silvia Ghilezan - 1996 - Notre Dame Journal of Formal Logic 37 (1):44-52.
A Classification of Intersection Type Systems.M. W. Bunder - 2002 - Journal of Symbolic Logic 67 (1):353-368.
The Emptiness Problem for Intersection Types.Pawel Urzyczyn - 1999 - Journal of Symbolic Logic 64 (3):1195-1215.
Grafted Frames and S1-Completeness.Beihai Zhou - 1999 - Journal of Symbolic Logic 64 (3):1324-1338.
A Union Catalogue of Philosophical Periodicals.Bikash Kumar Bhattacharya - 1989 - Indian Council of Philosophical Research in Association with Munshiram Manoharlal Publishers.
Plotinus, Mysticism, and Mediation.A. R. P. Robert - 2004 - Religious Studies 40 (2):145-163.
Inverse Problem for Cuts.Renling Jin - 2007 - Logic and Analysis 1 (1):61-89.
The Semantics of Entailment Omega.Yoko Motohama, Robert K. Meyer & Mariangiola Dezani-Ciancaglini - 2002 - Notre Dame Journal of Formal Logic 43 (3):129-145.
Economics and Ethics.Geoffrey Brennan & Daniel Moseley - forthcoming - In Hugh LaFollette (ed.), International Encyclopedia of Ethics. Wiley-Blackwell.

Monthly downloads

Added to index

2010-08-24

Total downloads

19 ( #259,934 of 2,172,599 )

Recent downloads (6 months)

1 ( #325,337 of 2,172,599 )

How can I increase my downloads?

My notes
Sign in to use this feature


Discussion
Order:
There  are no threads in this forum
Nothing in this forum yet.

Other forums