2014 | OriginalPaper | Buchkapitel
Process Types as a Descriptive Tool for Interaction
Control and the Pi-Calculus
verfasst von : Kohei Honda, Nobuko Yoshida, Martin Berger
Erschienen in: Rewriting and Typed Lambda Calculi
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.