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 and 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.




Phone: +49-176-3704-7666
TU Darmstadt
Hochschulstr. 10, 64289 Darmstadt, Germany
Office A307.
Email: gina.tcchen"@"gmail.com
my CV and dblp


Recent Research Works

"Lightening Global Types (Extended Version)". [Draft].

Abstract: 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. [paper].

Abstract: 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".
PLACES14, EPTCS Volume 155/2014, pages 38-46. [paper].

Abstract: 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, FORTE/FMOODS 2013, LNCS Volume 7892/2013, pages 50-65. [paper]. [full report].

Abstract: 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, to appear. COB2012, [paper].

Abstract: 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, Concur 2012, LNCS Volume 7454/2012, pages 209-224. [paper]. [full report]. [slide].

Abstract: 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. We demonstrate 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 observations, for both static and dynamic verifications. In particular, our theory offers a key criterion for suitability of specifications for distributed dynamic verifications.


"Asynchronous Distributed Monitoring for Multiparty Session Enforcement".
6th Trustworthy Global Computing, TGC 2011, LNCS Volume 7173/2012, pages 25-45. [paper]. [full report].

Abstract: 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.


scribble reference .

"Scribbling Interactions with a Formal Foundation".
7th Distributed Computing and Internet Technology 2011, ICDCIT 2011, LNCS Volume 6536/2011, Pages 55-75. [paper].

Abstract: 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.



PhD Thesis

Theories for Session-based Governance for Large-scale Distributed Systems.





Academic Activities

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 OOI deliverables



Interests

The pi-calculus.

Asynchronous session types.

Network monitoring.

Clouds computing

Financial engineering.

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.

Travelling.