Two session typing systems for higher-order mobile processes

Abstract

This paper proposes two typing systems for session interactions in higher-order mobile processes. Session types for the HOn-calculus capture high-level structures of communication 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. © Springer-Verlag Berlin Heidelberg 2007.