The paper Fair Termination of Binary Sessions (Ciccone & Padovani, 2022), written with Luca Ciccone, has been accepted at the 49th annual Symposium on Principles of Programming Languages (POPL 2022). In this work we study a type system that ensures the termination of binary sessions under strong fairness assumptions. The type system is the first using fair subtyping (Padovani, 2013; Padovani, 2016; Ciccone & Padovani, 2021), a liveness-preserving refinement of the classical subtyping relation for session types that has been studied extensively in the last years but was never applied in a type system. FairCheck is a proof-of-concept implementation of the type system described in the paper. You can read a draft of the paper online before it is officially published.
The GitHub repository of FairCheck is now publicly available. FairCheck is a proof-of-concept implementation of a type checker for a calculus of binary sessions such that well-typed processes are guaranteed to be fairly terminating. Fair termination is a generalized form of termination whereby all infinite executions of a process are deemed unrealistic because they violate some fairness assumption. The type system on which FairCheck is based is also the first one using fair subtyping (Padovani, 2013; Padovani, 2016; Ciccone & Padovani, 2021), a liveness-preserving refinement of the subtyping relation for session types.
The paper Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types (Ciccone & Padovani, 2021), written with Luca Ciccone, has been accepted at the 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). In this work we use generalized inference systems to specify combined safety and liveness properties of dependent session types mixing induction and coinduction. All the results have been formalized in Agda and are available on GitHub. Too bad the conference will be online only.
I'm an associate professor in Computer Science at the Computer Science Department of the University of Torino. ¶ My research interests lie in the areas of programming languages, type systems and concurrency theory. ¶ I'm the contact person of the FORMS research group on Formal Methods for Software Development.