Abstract
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. © 2014 Springer International Publishing Switzerland.
Cite
CITATION STYLE
Honda, K., Yoshida, N., & Berger, M. (2014). Process types as a descriptive tool for interaction control and the Pi-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8560 LNCS, pp. 1–20). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_1
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
