LANGUAGES AND MODELS FOR CONCURRENCY AND COMMUNICATION
January 01, 2021
Concurrency and communication are pervasive in modern software, but development tools still fail to support them, causing failures in protocol and service compliance or timing errors in resource usage and calling for novel programming abstractions and analysis methods. We introduced “Conversation types”, allowing multiparty interactions to be type-checked for deadlock-freedom and protocol compliance, leading to high impact publications. We have also developed type-based techniques to certify interface contracts, and analyse the behaviour of distributed transactions. Our works on deadlock-free session protocols is considered a seminal work on linear and session types, being the most cited CONCUR paper since 2010. We also developed new techniques to analyse concurrent programs manipulating shared state, based on behavioural types. This research has been developed in collaboration with CMU, INRIA, Imperial College, and Glasgow, and has led to publicly available prototypes, and highly visible publications in top venues such as POPL, ESOP, ECOOP, Inf&Comp, and ACM Surveys.
