Please be aware that links from outdated posts may be broken.


19 August 2022

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).

Distinguished Paper Award at ECOOP! Distinguished Paper Award at ECOOP!

08 June 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.

Fair Termination of Multiparty Sessions

30 April 2022

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 in Agda

22 March 2022

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.

TYPES 2022

05 March 2022

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.

Fair Termination of Binary Sessions

09 November 2021

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.


07 October 2021

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.

Inference Systems with Corules for Fair Subtyping

29 April 2021

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.

Workshop on Verification of Session Types

31 March 2021

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.

Invited speaker at ICTCS 2021

26 March 2021

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.

Fair Subtyping in Agda

07 February 2021

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.

Farewell Kube

29 November 2020

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.

An Introduction to Functional Programming in Haskell

23 November 2020

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.

FuSe on GitHub

11 November 2020

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.

DLπ Paper at PPDP 2020

03 July 2020

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.

Probabilistic Session Types

28 June 2020

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.


23 June 2020

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.

DLπ Released

19 May 2020

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.

New Home Page

25 April 2020

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.

Places Proceedings

01 April 2020

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.

PPDP 2009 – 2019

05 August 2019

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.

EasyJoin Released

07 April 2019

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.

EuroPar 2018

31 August 2018

Selected pictures of EuroPar 2018, which I co-chaired with Marco Aldinucci and Massimo Torquati, are now available online.

About Me

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.

Contact Information

Public Profiles