Timed Multiparty Session Types

Bocchi, Laura and Yang, Weizhen and Yoshida, Nobuko (2014) Timed Multiparty Session Types. In: Baldan, Paolo and Gorla, Daniele, eds. International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science. Springer pp. 419-434. (doi:https://doi.org/10.1007/978-3-662-44584-6_29) (Full text available)


We propose a typing theory, based on multiparty session types, for modular verification of real-time choreographic interactions. To model real-time implementations, we introduce a simple calculus with delays and a decidable static proof system. The proof system ensures type safety and time-error freedom, namely processes respect the prescribed timing and causalities between interactions. A decidable condition on timed global types guarantees time-progress for validated processes with delays, and gives a sound and complete characterisation of a new class of CTAs with general topologies that enjoys progress and liveness.

Item Type: Conference or workshop item (Paper)
Projects: Projects 0 not found.
Projects 0 not found.
Subjects: Q Science > QA Mathematics (inc Computing science) > QA299 Analysis, Calculus
Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Laura Bocchi
Date Deposited: 05 Nov 2014 10:17 UTC
Last Modified: 29 Nov 2016 18:08 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/43729 (The current URI for this page, for reference purposes)
Bocchi, Laura: https://orcid.org/0000-0002-7177-9395
  • Depositors only (login required):


Downloads per month over past year