Sciweavers

Share
TCS
2008

A typed lambda calculus with intersection types

8 years 5 months ago
A typed lambda calculus with intersection types
Intersection types are well-known to type theorists mainly for two reasons. Firstly, they type all and only the strongly normalizable lambda terms. Secondly, the intersection type operator is a meta-level operator, that is, there is no direct logical counterpart in the CurryHoward isomorphism sense. In particular, its meta-level nature implies that it does not correspond to the intuitionistic conjunction. The intersection type system is naturally a type inference system (system `a la Curry), but the meta-level nature of the intersection operator does not allow easily to design an equivalent typed system (system `a la Church). There are many proposals in the literature to design such systems, but none of them gives an entirely satisfactory answer to the problem. In this paper, we will review the main results in the literature both on the logical interpretation of intersection types and on proposed typed lambda calculi. The core of this paper is a new proposal for a true intersection ty...
Viviana Bono, Betti Venneri, Lorenzo Bettini
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TCS
Authors Viviana Bono, Betti Venneri, Lorenzo Bettini
Comments (0)
books