145
views
0
recommends
+1 Recommend
0 collections
0
shares
• Record: found
• Abstract: found
• Article: found
Is Open Access

# Intersection types for unbind and rebind

Preprint

Bookmark
There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

### Abstract

We define a type system with intersection types for an extension of lambda-calculus with unbind and rebind operators. In this calculus, a term with free variables, representing open code, can be packed into an "unbound" term, and passed around as a value. In order to execute inside code, an unbound term should be explicitly rebound at the point where it is used. Unbinding and rebinding are hierarchical, that is, the term can contain arbitrarily nested unbound terms, whose inside code can only be executed after a sequence of rebinds has been applied. Correspondingly, types are decorated with levels, and a term has type decorated with k if it needs k rebinds in order to reduce to a value. With intersection types we model the fact that a term can be used differently in contexts providing different numbers of unbinds. In particular, top-level terms, that is, terms not requiring unbinds to reduce to values, should have a value type, that is, an intersection type where at least one element has level 0. With the proposed intersection type system we get soundness under the call-by-value strategy, an issue which was not resolved by previous type systems.

### Most cited references11

• Record: found

### LCF considered as a programming language

(1977)
Bookmark
• Record: found

### MetaML and multi-stage programming with explicit annotations

(2000)
Bookmark
• Record: found

### An extension of the basic functionality theory for the $\lambda$-calculus.

(1980)
Bookmark

### Author and article information

###### Journal
23 January 2011
###### Article
10.4204/EPTCS.45.4
1101.4426

EPTCS 45, 2011, pp. 45-58
In Proceedings ITRS 2010, arXiv:1101.4104
cs.LO cs.PL
EPTCS