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

• Type: Journal
• Year: 2008
• Where: TCS
• Authors: Viviana Bono, Betti Venneri, Lorenzo Bettini
• Keywords: Intersection Type, Meta-level, Meta-level Nature, TCS 2008, Theoretical Computer Science