Please be aware that links from outdated posts may be broken.
The paper An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus has been accepted at the 33rd International Conference on Concurrency Theory (CONCUR 2022).
The paper Fair Termination of Multiparty Sessions is one out of three distinguished papers at the 36th European Conference on Object-Oriented Programming (ECOOP 2022). In the picture Luca Ciccone receives the award from Karim Ali at the ceremony.
The paper Fair Termination of Multiparty Sessions, written with Luca Ciccone and Francesco Dagnino, has been accepted at the 36th European Conference on Object-Oriented Programming (ECOOP 2022). This is a follow up of previous work in which we apply our technique ensuring fair termination to multiparty sessions. In this work we also present a new sound and complete characterization of fair subtyping which is substantially simpler than previous ones and does not require auxiliary definitions or the use of a generalized inference system.
Fair termination is a termination property weaker than strong termination but stronger than weak termination in which only the “fair” executions of a system are considered insofar as termination is concerned, whereas “unfair” executions are considered to be unrealistic. For a particular fairness assumption, it is possible to provide a sound and complete characterization of fair termination that does not mention fair executions. The FairTermination module is an Agda formalization of this notion of fair termination along with soundness and completeness proofs of its characterization.
I’m pleased to be a programme committee member of the 28th International Conference on Types for Proofs and Programs (TYPES 2022), looking forward to a bunch of exciting submissions and intriguiting talks by the invited speakers.
The paper Fair Termination of Binary Sessions, 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, 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.
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, 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, 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.
Luca Ciccone and I have been working for some time on proof systems for fair subtyping and other liveness properties of dependent session types using generalized inference systems, which are inference systems enriched with corules. You can see the Agda formalization of these proof systems on GitHub.
The Kube framework that my web site was based on has become obsolete. Given the simplicity of this site I decided to write my own stylesheet and to rely on Frow CSS for just grids and buttons. Make sure you empty the cache of your browser if these pages look odd.
This year I taught the lab sessions of my course on functional programming online. I prepared some lecture notes mixing cards (small pages focusing on a single Haskell feature) and case studies (large exercises solving a programming problem). The final version of the notes is publicly available on GitHub. Thanks to all the students who provided feedback and notified me of errors.
While updating my home page and the repositories of my software projects I thought it would be a good idea to move FuSe on GitHub, making it easier for anyone interested to use it and possibly contribute further developments.
The paper A Dependently Typed Linear π-Calculus in Agda, written with Luca Ciccone, has been accepted to PPDP 2020. The submitted version of the paper is available here and Luca Ciccone has already given a talk about DLπ at the VEST 2020 workshop.
The paper Probabilistic Analysis of Binary Sessions, written with Omar Inverso, Hernán Melgratti, Catia Trubiani and Emilio Tuosto has been accepted to CONCUR 2020. There we study a refinement of session types related to a family of discrete-time Markov chains that enables the reasoning on the probability of successful session termination.
Unfortunately ETAPS 2020 is officially cancelled and so is PLACES 2020 as a consequence. It’s a pity that authors of accepted papers won’t have the opportunity to present their work at the workshop. There is a currently open call for a JLAMP Special Issue dedicated to the topics of the workshop.
This date marks the first public release of DLπ, an Agda formalization of the linear π-calculus with dependent pairs jointly developed with Luca Ciccone. DLπ allows for the modeling of data-dependent processes and protocols encompassing dependent session types. Luca Ciccone will give a talk about DLπ at the VEST workshop.
My home page had been overdue for a restyling for quite some time when I stumbled across the gorgeous home page of Greg Restall, so I decided to restyle my home page like his own. Some content that used to be reachable from the old home page is temporarily unavailable, work is in progress to restore everything.
I’m chairing PLACES 2020 together with Stephanie Balzer. The proceedings of the workshop have been published and are available here. Note that, due to the COVID-19 spread, ETAPS 2020 has been postponed to some future date which is not known yet at this time.
The paper Foundations of Session Types, which I coauthored with Giuseppe Castagna, Mariangiola Dezani-Ciancaglini and Elena Giachino back in 2009, has won the PPDP Most Influential Paper 10-Year Award. We have written an abstract to recollect how that work was born and what has happened in the meantime.
TypeState-Oriented Programming (TSOP) is a programming methodology for implementing objects with a state-sensitive public interface. EasyJoin is a code generator that allows Java programmers to use concurrent TSOP when implementing and using object with state-sensitive interfaces.
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.