Intersection types for lambda-terms and combinators and their logics

Logic Journal of the IGPL 10 (4):357-378 (2002)
  Copy   BIBTEX

Abstract

It is well known that the simple types of closed lambda terms or combinators can be interpreted as the theorems of intuitionistic implicational logic . Venneri, using an equivalence between the intersection type system for lambda calculus, without the universal type ω, TA∧λ, and a similar system for combinators, TA∧, shows that the types of TA∧λ are the theorems of a Hilbert-style sublogic of the → ∧ fragment of H→.In this paper we fill a gap in the equivalence proof and introduce a new system of intersection types for lambda calculus that is weaker than TA∧λ, but has the same set of types. The new system has the advantage that the logic of types can be obtained directly from the rules - just as H→ can be obtained from simple type theory

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 74,480

External links

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

Through your library

Similar books and articles

Strong Normalization and Typability with Intersection Types.Silvia Ghilezan - 1996 - Notre Dame Journal of Formal Logic 37 (1):44-52.
The Proofs of $Alpha Rightarrow Alpha$ in $P - W$.Sachio Hirokawa - 1996 - Journal of Symbolic Logic 61 (1):195-211.
A Classification of Intersection Type Systems.M. W. Bunder - 2002 - Journal of Symbolic Logic 67 (1):353-368.
Inductive Types and Type Constraints in the Second-Order Lambda Calculus.Nax Paul Mendler - 1991 - Annals of Pure and Applied Logic 51 (1-2):159-172.
The Church-Rosser Property in Dual Combinatory Logic.Katalin Bimbó - 2003 - Journal of Symbolic Logic 68 (1):132-152.
Kripke-Style Models for Typed Lambda Calculus.John C. Mitchell & Eugenio Moggi - 1991 - Annals of Pure and Applied Logic 51 (1-2):99-124.

Analytics

Added to PP
2015-02-04

Downloads
12 (#797,852)

6 months
1 (#417,896)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

A Classification of Intersection Type Systems.M. W. Bunder - 2002 - Journal of Symbolic Logic 67 (1):353-368.

Add more citations

References found in this work

No references found.

Add more references