Please be aware that links from outdated posts may be broken.
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 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 (Padovani, 2017) 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 (Ciccone & Padovani, 2020), 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 (Inverso et al., 2020), 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 (Balzer & Padovani, 2020). 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 (Castagna et al., 2009), 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 (Castagna et al., 2019) 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 (Gerbo & Padovani, 2019) 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 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.