Abstract:
The lambda-calculus with resources is a non-deterministic refinement of the lazy lambda-calculus which provides explicit means to control the number of times an argument can be used, and introduces the possibility of raising deadlocks during evaluation. It arose in connection with Milner's encoding of lazy lambda-calculus into the pi-calculus and proved to be the correct extension to study the semantics induced by the pi-calculus over pure lambda-terms. In this paper, we study a functionality theory in the style of Coppo et al.'s intersection type system for the calculus of resources extended with convergence testing. The interpretation of terms in this typing system gives rise to a fully abstract semantics of the calculus. This is shown following the definability approach. We also prove that this semantics is not fully abstract for the calculus without convergence testing.