Process Types as a Descriptive Tool for Interaction (with Kohei HondaNobuko Yoshida)

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.

Download: Publisher's version, authors' draft. Published in Proc. RTA-TLCA 2014 (BibTeX).