in Theoretical Computer Science

Dept. Computer Science

Queen Mary College,

University of London, UK

During my PhD program, I studied the π-calculus and theories of session types. The former establishes a calculus for modelling mobility whereas the latter establishes a typing discipline for structuring interactions to a meaningful session (i.e., communication). My main research activities during this period were as follows:

Session-based Governance

My thesis “Theories for Session-based Governance for Large-scale Distributed Systems” introduced principles of specifications and verifications to formalize the logical properties for interactional behaviors among multiparty communication. Governance is a general term for specifying the appropriate mutual behaviors, monitoring interactions against specifications, and taking actions when non-compliant behaviors are detected. I proposed a process calculus for a session-based distributed monitoring framework to dynamically govern cross-domain interactions; furthermore, I proposed typing principles for ensuring well-behaved interactions among processes. The properties of global safety, global transparency, and session fidelity are stated and proved. These results were published in the international workshop TGC 2011 and the international conference FMOODS/FORTE 2013; a journal paper was published by the Journal of Theoretical Computer Science (TCS) in 2017.

Specifying Stateful Session Types

Under the supervision of Professor Kohei Honda, I discovered that embedding states into specifications (i.e., stateful specifications) to asynchronously monitor interactions may generate mistakes, which appear when we assert the operation of endpoints’ ghost states into monitors. We offered a fine-grained syntax and semantics of specifications with stateful assertions and proved the properties of well-formed specifications to monitor asynchronous interactions. This result was published in the international conference CONCUR 2012. 

Please reload


T: (+49) 06151-16-27813