A typed lambda calculus with intersection types
| Autor: | Viviana Bono, Betti Venneri, Lorenzo Bettini |
|---|---|
| Rok vydání: | 2008 |
| Předmět: |
Simply typed lambda calculus
General Computer Science System F Church style Parallelism Type inference Intersection types Typed Lambda Calculus Intersection Types Type Inference Strong and weak typing Dependent type Theoretical Computer Science Pure type system Algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Curry style Computer Science::Programming Languages Typed lambda calculus Shared resources Type constructor Computer Science(all) Lambda calculus Mathematics |
| Zdroj: | Theoretical Computer Science. 398:95-113 |
| ISSN: | 0304-3975 |
| Popis: | 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 Curry–Howard 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 à la Curry), but the meta-level nature of the intersection operator does not allow to easily design an equivalent typed system (system à 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 typed lambda calculus, without any meta-level notion. Namely, any typable term (in the intersection type inference) has a corresponding typed term (which is the same as the untyped term by erasing the type decorations and the typed term constructors) with the same type, and vice versa.The main idea is to introduce a relevant parallel term constructor which corresponds to the intersection type constructor, in such a way that terms in parallel share the same resources, that is, the same context of free typed variables. Three rules allow us to generate all typed terms. The first two rules, Application and Lambda-abstraction, are performed on all the components of a parallel term in a synchronized way. Finally, via the third rule of Local Renaming, once a free typed variable is bounded by lambda-abstraction, each of the terms in parallel can do its local renaming, with type refinement, of that particular resource. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect