Speaker / Predavač :
Mariangiola Dezani
Title / Naslov:
On the Preciseness of Subtyping in Session Types
Abstract / Abstrakt:
The subtyping systems of mobile processes have been extensively studied since early 1990s as one of the most applicable concepts in the types for concurrency. Their correctness has been usually provided as the soundness of subtyping relations with respect to the type safety. The converse direction, the completeness, has been largely ignored in spite of its usefulness to define the greatest subtyping relation possible without violating type safety, solely based on operational semantics.
This talk discusses a technique for formalising and proving that a subtyping system is precise (i.e. both sound and complete) with respect to the type safety in the pi-calculus, and applies it to synchronous and asynchronous session calculi.
The well-known session subtyping, the branching-selection subtyping, turns out to be sound and complete in the synchronous calculus. Instead in the asynchronous calculus, this common subtyping is incomplete with respect to the type-safety: that is, there exist session types T and S such that T can safely be considered as a subtype of S, but T is not a subtype of S. We then propose an asynchronous subtyping system which is sound and complete with respect to the asynchronous calculus. The method gives a general guidance to design rigorous channel-based subtyping systems with respect to desired safety properties