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 happy to serve as PC member for the 2nd workshop on Verification of Session Types (VEST 2021), organized by Ornela Dardha and António Ravara as an (online) satellite event of ICALP 2021. The first edition of the workshop was very successful and I’m sure this edition will be just as good.
I’m honored to be one of the invited speakers of the 22nd Italian Conference on Theoretical Computer Science which is being organized by the University of Bologna and will be held virtually in September.
I'm an associate professor 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.