Title: Full abstraction for lambda calculus with resources and convergence testing
Abstract: The calculus with resources is a non-deterministic refinement of lazy λ calculus which provides explicit means to control the number of times an argument can be used [6], and introduces the possibility of raising deadlocks during evaluation. It arose in connection with Milner's encoding of lazy lambda calculus into π calculus and proved to be the correct extension to study the semantics induced by π-calculus over pure λ-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.
Publication Year: 1996
Publication Date: 1996-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 6
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot