I’m happy to be a programme committee member of the International Conference on Types for Proofs and Programs (TYPES 2023) for the second year in a row. Check the call for papers for details about submissions and deadlines.
It was a great pleasure to deliver an invited talk at the Forum Numerica seminar series today. You can find the slides in the talks section of this site.
Client-server sessions are based on a variation of the traditional interpretation of linear logic propositions as session types in which non-linear channels are typed by coexponentials instead of the usual exponentials. In this manuscript I prove a fair termination result for CSLL∞, a core calculus of client-server sessions. Each well-typed CSLL∞ process corresponds to a proof in μMALL∞, the infinitary proof theory of linear logic with least and greatest fixed points. Fair termination in CSLL∞ follows from cut elimination in μMALL∞.
I'm an associate professor in Computer Science at the Computer Science Division of the School of Science and Technology of the University of Camerino. My research interests span both theory and practice in the areas of programming languages, type systems, concurrency theory, distributed computing and formal verification.