π-calculus, Session Types research at the University of Oxford
Modular methodologies for the development and verification of concurrent/distributed systems are increasingly relevant nowadays. We investigate the simultaneous composition of multiple systems in a multiparty-session-type setting, working on suitable notions of interfacing policy and multicompatibility. The resulting method is conservative (it makes only the strictly needed changes), flexible (any system can be looked at as potentially open) and safe (relevant communication properties, e.g. lock-freedom, are preserved by composition). We obtain safety by proving preservation of typability. We also provide a sound and complete type inference algorithm.
@inproceedings{BDGY2023,
author = {Franco Barbanera and Mariangiola Dezani-Ciancaglini and Lorenzo Gheri and Nobuko Yoshida},
title = {{Multicompatibility for Multiparty-Session Composition}},
booktitle = {Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming},
pages = {1--15},
publisher = {Association for Computing Machinery},
year = 2023
}
@inproceedings{BDGY2023,
author = {Franco Barbanera and Mariangiola Dezani-Ciancaglini and Lorenzo Gheri and Nobuko Yoshida},
title = {{Multicompatibility for Multiparty-Session Composition}},
booktitle = {Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming},
pages = {1--15},
publisher = {Association for Computing Machinery},
doi = "10.1145/3610612.3610614",
year = 2023
}