HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Lazy functions and mobile processes

Davide Sangiorgi 1
1 MEIJE - Concurrency, Synchronization and Real-time Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This paper continues the study of Milner's encoding of the lazy $\lambda$-calculus into the $\pi$-calculus \cite{Mil92}. The encoding is shown to give rise to a $\lambda$-model in which, in accordance with the theory of the lazy $\lambda$-calculus, conditional extensionality holds. However, the model is not fully abstract. To obtain full abstraction, the operational equivalence on $\lambda$-terms ({\em applicative bisimulation}) is refined. The new relation, called {\em open applicative bisimulation}, allows us to observe some internal structure of $\lambda$-terms, and coincides with the {\em Lévy-Longo Tree} equality. Milner's encoding is presented on a sublanguage of the $\pi$-calculus similar to those proposed by Boudol \cite{Bou92}, Honda and Tokoro \cite{HoTo91}. Some properties of bisimulation on this sublanguage are demonstrated and used to simplify a few proofs in the paper. For instance, {\em ground bisimulation}, a form of bisimulation where no name instantiation on input actions is required, is proved to be a congruence relation; as a corollary, various $\pi$-calculus bisimilarity equivalences (ground, late, early, open) are shown to coincide on this sublanguage.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:39:04 PM
Last modification on : Friday, February 4, 2022 - 3:19:39 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:28:20 PM


  • HAL Id : inria-00074163, version 1



Davide Sangiorgi. Lazy functions and mobile processes. RR-2515, INRIA. 1995. ⟨inria-00074163⟩



Record views


Files downloads