Timed Session Types
Massimo Bartoletti, Tiziana Cimoli, Maurizio Murgia

TL;DR
This paper introduces timed session types to formalize timed communication protocols, providing a decidable compliance relation and methods to determine and construct compliant session types, including subtyping.
Contribution
It presents a sound and complete technique for deciding compliance and constructing the most precise compliant session type, extending untimed session type concepts to the timed setting.
Findings
Decidability of compliance between timed session types.
Method to construct the most precise compliant session type.
Decidability of subtyping based on compliance.
Abstract
Timed session types formalise timed communication protocols between two participants at the endpoints of a session. They feature a decidable compliance relation, which generalises to the timed setting the progress-based compliance between untimed session types. We show a sound and complete technique to decide when a timed session type admits a compliant one. Then, we show how to construct the most precise session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
