Intersection types for unbind and rebind

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

Full description

Bibliographic Details
Main Authors: Mariangiola Dezani-Ciancaglini, Paola Giannini, Elena Zucca
Format: Article
Language:English
Published: Open Publishing Association 2011-01-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1101.4426v1