Advertisement
Published in:
2014 | OriginalPaper | Chapter
Process Types as a Descriptive Tool for Interaction
Control and the Pi-Calculus
Authors : Kohei Honda, Nobuko Yoshida, Martin Berger
Published in: Rewriting and Typed Lambda Calculi
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We demonstrate a tight relationship between linearly typed
π
-calculi and typed
λ
-calculi by giving a type-preserving translation from the call-by-value
λμ
-calculus into a typed
π
-calculus. The
λμ
-calculus has a particularly simple representation as typed mobile processes. The target calculus is a simple variant of the linear
π
-calculus. We establish full abstraction up to maximally consistent observational congruences in source and target calculi using techniques from games semantics and process calculi.