recent news

DLπ paper at ppdp 2020

03 July 2020

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.

probabilistic session types

28 June 2020

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.

etaps and places 2020

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.

selected publications

  • Omar Inverso, Hernán Melgratti, Luca Padovani, Catia Trubiani, Emilio Tuosto, Probabilistic Analysis of Binary Sessions, Proceedings of the 31st International Conference on Concurrency Theory (CONCUR’20), 2020. bib
  • Luca Padovani, Context-Free Session Type Inference, ACM Transactions on Programming Languages and Systems, vol. 41(2), pages 9:1-9:37, 2019. doi bib
  • Ugo de’Liguoro, Luca Padovani, Mailbox Types for Unordered Interactions, Proceedings of the 32nd European Conference on Object-Oriented Programming (ECOOP’18), pages 15:1-15:28, 2018. doi bib

teaching - insegnamento

Il ricevimento studenti avviene previo appuntamento da prenotare con almeno un giorno di anticipo. Per ogni insegnamento x, non effettuo ricevimento di x nei tre giorni lavorativi precedenti un appello di x. In questo anno accademico insegno: