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.

• Type: Conference
• Year: 2007
• Where: TLCA
• Authors: Dimitris Mostrous, Nobuko Yoshida
• Keywords: Code Mobility, Session Interactions, Session Types, Theoretical Computer Science, TLCA 2007