Tzu-chun Chen (Gina Chen), Postdoctoral Researcher
I got the PhD degree of Computer Science at Queen Mary College, University of London in 2013
under the support of UK government's EPSRC full studentship.
I was very lucky and grateful to have
Prof. Kohei Honda,
as my supervisor and
Prof. Nobuko Yoshida
as my co-supervisor during my PhD studies.
In my PhD, I studied computing theories and focus on formal methods, session types,
the pi-calculus, and the theorems of concurrency and distributed computing.
From 1st September 2013 to 31st August 2014, I have worked with
Prof. Mariangiola Dezani
Dr. Luca Padovani
as a research fellow in the Department of Computer Science, at University of Turin
(Universita di Torino).
I studied various aspects of session types,
covering subtyping, the composability of session types, and the structure of session-based policies with
temporal logics. I also studied combinatory logics, type reconstruction and intersection types.
Since 1st September 2014,
I have worked with
Prof. Patrick Eugster
as a postdoctoral researcher
for a joint project, LiveSoft, conducted by TU Darmstadt (Germany) and Purdue University (USA).
In the lastest work,
we designed a programming language which
equipes with robust exception-handling capability,
and leaves the exception-independent interactions unaffected once an exception occurs.
Currently I am aiming on
designing concurrent programming languages for large-scale distributed systems
through modelling concurrent/asynchronous interactions among distributed endpoints,
and establishing type systems for distributedly compiling interactions.
64289 Darmstadt, Germany
my CV and
Recent Research Works
"Lightening Global Types (Extended Version)".
The novelty of this paper is a method for
lightening (i.e. decomposing) complicated global types
by removing redundant interactions and preserving the order of the remaining interactions.
This method produces modularised global types
which are invoked by the call constructor
and together preserve the meaning of the original type.
This work extends
the work published in PLACES14
by improving and simplifying the lightening functions and by adding:
1. local types as projections of light global types,
2. a calculus of asynchronous processes implementing light global types,
3. a type system for assigning the local types of point 1 to the processes of point 2,
4. the proof of subject recursion for the type system of point 3.
"On the Preciseness of Subtyping in Session Types".
PPDP2014. To appear.
Subtyping in concurrency has been extensively studied since early 1990s as one of the most interesting issues in type theory. The correctness of subtyping relations has been usually provided as the soundness for type safety. The converse direction, the completeness, has been largely ignored in spite of its usefulness to define the greatest subtyping relation ensuring type safety. This paper formalises preciseness (i.e. both soundness and completeness) of subtyping for mobile processes and studies it for the synchronous and the asynchronous session calculi. We first prove that the well-known session subtyping, the branching- selection subtyping, is sound and complete for the synchronous calculus. Next we show that in the asynchronous calculus, this subtyping is incomplete for type-safety: that is, there exist session types T and S such that T can safely be considered as a subtype of S, but this fact is not derivable by the subtyping. We then propose an asynchronous subtyping system which is sound and complete for the asynchronous calculus. The method gives a general guidance to design rigorous channel-based subtypings respecting desired safety properties.
"Lightening Global Types".
EPTCS Volume 155/2014, pages 38-46.
Global session types prevent participants from waiting for never coming messages. Some interactions take place just for the purpose of informing receivers that some message will never arrive or the session is terminated. By decomposing a big global type into several light global types, one can avoid such kind of redundant interactions. Lightening global types gives us cleaner global types, which keep all necessary communications. This work proposes a framework which allows to easily decompose global types into light global types, preserving the interaction sequences of the original ones but for redundant interactions.
"Monitoring Networks through Multiparty Session Types".
2013 IFIP Joint International Conference,
LNCS Volume 7892/2013, pages 50-65.
In large-scale distributed infrastructures, applications are realised through communications among distributed components. The need for methods for assuring safe interactions in such environments is recognised, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored pi-calculus with dynamic usage of multiparty session types (MPST), offering a rigorous foundation for safety assurance of distributed components which asynchronously communicate through multiparty sessions. Our theory establishes a framework for semantically precise decentralised run-time enforcement and provides reasoning principles over monitored distributed applications, which complement existing static analysis techniques. We introduce asynchrony through the means of explicit routers and global queues, and propose novel equivalences between networks, that capture the notion of interface equivalence, i.e. equating networks offering the same services to a user. We illustrate our static-dynamic analysis system with an ATM protocol as a running example and justify our theory with results: satisfaction equivalence, local/global safety and transparency, and session fidelity.
"Structuring Communication with Session Types".
2012 Concurrent Objects and Beyond: From Theory to High-Performance Computing,
Session types are types for distributed communicating
processes. They were born from process encodings of data structures
and typical interaction scenarios in an asynchronous version of the
pi-calculus, and are being studied and developed as a potential
basis for structuring concurrent and distributed computing, as well
as in their own right. In this paper, we introduce basic ideas of
sessions and session types, outline their key technical elements,
and discuss how they may be usable for programming, drawing from our
experience and comparing with existing paradigms, especially
concurrent objects such as actors. We discuss how session types can
offer a programming framework in which communications are structured
both in program text and at run-time.
"Specifying Stateful Asynchronous Properties for Distributed Programs".
23rd International Conference on Concurrency Theory,
LNCS Volume 7454/2012, pages 209-224.
Having stateful specifications to track the states of processes,
such as the balance of a customer for online shopping
or the booking number of a transaction, is needed to verify
real-life interacting systems. For safety assurance of
distributed IT infrastructures, specifications need to capture
states in the presence of asynchronous interactions.
that not all specifications are suitable for asynchronous
observations because they implicitly rely on an order-preservation
assumption. To establish a theory of asynchronous specifications, we
use the interplay between synchronous and asynchronous semantics,
through which we characterise the class of specifications
suitable for verifications through asynchronous interactions. The
resulting theory offers a general semantic setting as well as
concrete methods to analyse and determine semantic well-formedness
(healthiness) of specifications with respect to asynchronous
for both static and dynamic verifications.
In particular, our theory offers a key criterion for
suitability of specifications for distributed dynamic
"Asynchronous Distributed Monitoring for Multiparty Session Enforcement".
6th Trustworthy Global Computing,
LNCS Volume 7173/2012, pages 25-45.
We propose a formal model of runtime safety enforcement for large-scale, cross-language distributed applications with possibly untrusted endpoints. The underlying theory is based on multiparty session types with logical assertions (MPSA), an expressive protocol specification language that supports runtime validation through monitoring. Our method starts from global specifications based on MPSAs which the participants should obey. Distributed monitors use local specifications, projected from global specifications, to detect whether the interactions are well-behaved and take appropriate actions, such as suppressing illegal messages.We illustrate the design of our model with examples from real-world distributed applications. We prove monitor transparency, communication conformance, and global session fidelity in the presence of possibly unsafe endpoints.
"Scribbling Interactions with a Formal Foundation".
7th Distributed Computing and Internet Technology 2011,
LNCS Volume 6536/2011, Pages 55-75.
In this paper we discuss our ongoing endeavour to apply notations and algorithms based on the pi-calculus and its theories for the development of large-scale distributed systems. The execution of a large- scale distributed system consists of many structured conversations (or sessions) whose protocols can be clearly and accurately specified using a theory of types for the pi-calculus, called session types. The proposed methodology promotes a formally founded, and highly structured, development framework for modelling and building distributed applications, from high-level models to design and implementation to static checking to runtime validation. At the centre of this methodology is a formal description language for representing protocols for interactions, called Scribble. We illustrate the usage and theoretical basis of this language through use cases from different application domains.
Theories for Session-based Governance for Large-scale Distributed Systems.
Research fellow of Lambda group
in Department of Informatics, University of Torino.
From 2013 to now.
A research member of project
scribble . From 2010 to now.
A research member of project
Ocean Observatories Initiative (OOI) cyber-infrastructure.
From Oct 2009 to Feb 2013.
London OOI Meeting
Asynchronous session types.
High performance computing for options.
Musical and play.
Classic. Chopin, Mozart, Rachmaninoff, etc..
Pop musics. Mike Oldfield, Cold Play, Eminem, Jam Hsiao.
Eating. Especially chocolate. And searching good chocolate stores.