Postdoctoral Researcher 

In Formal Method of Computing

Dept. Informatica,

Universit ́a di Torino, Italy 

On the Preciseness of Subtyping in Session Types

In collaboration with Prof. Dezani-Ciancaglini, Prof. Yoshida, and Dr. Scalas, we investigated the theories of subtyping relations, which lead to a practical purpose: When a local service (in a network) needs to change or be updated, we know what kinds of new service can be adopted to ensure that other interacting parties still work without errors (communication safety). For mobile processes modeled by the synchronous and asynchronous session calculi, we studied both the soundness for type safety and the completeness for defining the greatest subtyping relation ensuring type safety. This work was published in the international conference PPDP 2014 and has been accepted by the journal LMCS. 

Lightening Global Types

In this work, we designed an encoding to transform a multiparty session type into a set of binary session types linked by causality-preserving declarations (shortly written as BSd types). We investigated whether the well-typed processes with respect to BSd types are reversible or not. An algorithm was developed to lighten a complicated global type into several simpler and smaller global types linked by declarations preserving the causalities of the original global type.

Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear pi-Calculi

In collaboration with Prof. Padovani and Mr. Tosatto, we studied type reconstruction for a type system guaranteeing deadlock freedom and lock freedom for well-typed processes, presented by a linear π-calculus. In this work, we assumed that communication is carried by channels, which are associated with levels and tickets. We specified how channels annotated with levels and tickets can be used by communicating processes to be deadlock-free and lock-free. As it is unrealistic to assume that a programmer is able to manipulate the rank of levels and tickets by hand in any non-trivial process, having a type reconstruction algorithm to automatically calculate the set of possible ranks for each channel is practically useful. This work was published in COORDINATION 2015

Mixin Composition Synthesis Based on Intersection Types

In collaboration with Mr. Bessai, Mr. Dudenhefner, Prof. Düdder, Prof. de’Liguoro, and Prof. Rehof, we worked on synthesizing compositions of mixins using type inhabitation in intersection types. In this work, the classes and mixins are expressed by lambda calculus with records. This result was published in conference TLCA 2015.

Please reload

During this period, I studied various aspects of behavioral types covering subtyping, the composability of session types, and the structure of session-based policies with temporal logics. I also worked on type reconstruction, intersection types, and combinatory logics. 


T: (+49) 06151-16-27813