π-calculus, Session Types research at the University of Oxford
Session types express a protocol which specifies the order and type of messages exchanged by concurrently executing processes. Prior work has been adapted to many frameworks including Agha’s work [10], which has successfully extended session types to model distributed asyn- chronous multi-actors. Most works on session types, including Agha’s work, take an equi-recursive approach and do not distinguish among a recursive type and its unfolding. One main problem of an equi-recursive type system is that its mechanisation in proof assistants is utterly com- plex and eventually requires co-induction. To overcome this problem, this paper presents an iso-recursive type system for binary sessions based on a novel congruence on types which relates recursive types and their un- folding. Our system based on type congruence enables to use a simple syntactic-directed duality without complicating the typability of pro- cesses. We mechanise the type congruence relation in Rocq without re- sorting to coinductive types, and use the proof assistant to show that our iso-recursive typing system satisfies subject reduction.
@inproceedings{GY2025,
author = {Marco Giunti and Nobuko Yoshida},
title = {{Type Congruence, Duality and Iso-Recursive Binary Session Types}},
booktitle = {Essay Dedicated to Prof. Gul Agha to Celebrate his Scientific Career},
pages = {--},
publisher = {Springer Nature Computer Science book series},
year = 2025
}
@inproceedings{GY2025,
author = {Marco Giunti and Nobuko Yoshida},
title = {{Type Congruence, Duality and Iso-Recursive Binary Session Types}},
booktitle = {Essay Dedicated to Prof. Gul Agha to Celebrate his Scientific Career},
pages = {--},
publisher = {Springer Nature Computer Science book series},
year = 2025
}