The "Relevance" of Intersection and Union Types

Notre Dame Journal of Formal Logic 38 (2):246-269 (1997)


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

Download options


    Upload a copy of this work     Papers currently archived: 72,856

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

30 (#386,176)

6 months
1 (#386,040)

Historical graph of downloads
How can I increase my downloads?

References found in this work

A Propositional Calculus with Denumerable Matrix.Michael Dummett - 1959 - Journal of Symbolic Logic 24 (2):97-106.
The Semantics of Entailment — III.Richard Routley & Robert K. Meyer - 1972 - Journal of Philosophical Logic 1 (2):192 - 208.
Concerning Formulas of the Types a →B ∨C, a →(Ex)B(X).Ronald Harrop - 1960 - Journal of Symbolic Logic 25 (1):27-32.
Algebraic Analysis of Entailment I.Robert K. Meyer & Richard Routley - 1972 - Logique Et Analyse 15 (59/60):407-428.
Domain Theory in Logical Form.Samson Abramsky - 1991 - Annals of Pure and Applied Logic 51 (1-2):1-77.

View all 10 references / Add more references

Citations of this work

The Emptiness Problem for Intersection Types.Paweł Urzyczyn - 1999 - Journal of Symbolic Logic 64 (3):1195-1215.

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.Paweł 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.