Sciweavers

TLCA
2007
Springer

Two Session Typing Systems for Higher-Order Mobile Processes

13 years 9 months ago
Two Session Typing Systems for Higher-Order Mobile Processes
Abstract. This paper proposes two typing systems for session interactions in higherorder mobile processes. Session types for the HOπ-calculus capture high-level structures nication protocols and code mobility as type abstraction, and can be used to statically check the safe and consistent process composition in communication-centric distributed software. Integration of arbitrary higher-order code mobility and sessions leads to technical difficulties in type soundness, because linear usage of session channels and completion of sessions are required in executed code. By using techniques from the linear λ-calculus, we develop a coherent and tractable session typing system for the HOπ-calculus. We also present an alternative system based on fine-grained process types. The formal comparison between the two systems offers insight on the interplay between higher-order code mobility and session types.
Dimitris Mostrous, Nobuko Yoshida
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TLCA
Authors Dimitris Mostrous, Nobuko Yoshida
Comments (0)