Process types as a descriptive tool for interaction

Honda, Kohei, Yoshida, Nobuko and Berger, Martin (2014) Process types as a descriptive tool for interaction. Rewriting and Typed Lambda Calculi. RTA 2014, Vienna, Austria, 14-17 July 2014. Published in: Rewriting and Typed Lambda Calculi. RTA 2014. 1-20. Springer ISBN 9783319089171

[img] PDF - Accepted Version
Download (409kB)

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.

Item Type: Conference Proceedings
Schools and Departments: School of Engineering and Informatics > Informatics
Research Centres and Groups: Foundations of Software Systems
Depositing User: Martin Berger
Date Deposited: 18 Dec 2017 15:37
Last Modified: 18 Dec 2017 15:38
URI: http://sro.sussex.ac.uk/id/eprint/72278

View download statistics for this item

📧 Request an update