Paper Info
Title
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 HOπ-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.
Year
DOI
Venue
2007
10.1007/978-3-540-73228-0_23
TLCA
Keywords
Field
DocType
alternative system,higher-order code mobility,higher-order mobile process,executed code,session channel,code mobility,session interaction,arbitrary higher-order code mobility,tractable session,session type,programming language,type system,software integration,functional language,distributed computing,operating system,communication protocol,distributed application,higher order,e commerce
Programming language,Process composition,Abstraction,Computer science,Communication channel,Code mobility,Soundness,Round-trip delay time,Distributed computing,Communications protocol
Conference
Volume
ISSN
Citations 
4583
0302-9743
21
PageRank 
References 
Authors
0.91
18
2
Name
Order
Citations
PageRank
Dimitris Mostrous11306.37
Nobuko Yoshida22607153.29