MobilityReadingGroup

Asynchronous Timed Session Types
from duality to time-sensitive processes

Laura BOCCHI, Maurizio MURGIA, Vasco THUDICHUMVASCONCELOS, Nobuko YOSHIDA

We present a behavioural typing system for a higher-order timed calculus, using session types to model timed protocols, and the calculus to abstract implementations. Behavioural typing ensures that processes in the calculus will perform actions in the time-windows prescribed by their protocols. We introduce duality and subtyping for timed asynchronous session types. Duality includes a class of protocols that previous work on asynchronous timed session types could not type-check. Subtyping is critical for precision of our typing system, especially for session delegation. The composition of dual (timed asynchronous) types enjoys progress when using an urgent receive semantics, in which receive actions are executed as soon as the expected message is available. Our calculus increases the modelling power of calculi used in the previous work on timed sessions, adding a blocking receive primitive with timeout, and a primitive that consumes an arbitrary amount of time in a given range.

@inproceedings{BMVY2019,
  author = {Laura Bocchi and Maurizio Murgia and Vasco Thudichum Vasconcelos and Nobuko Yoshida},
  title = {{Asynchronous Timed Session Types}},
  booktitle = {28th European Symposium on Programming},
  series = {LNCS},
  volume = {11423},
  pages = {583--610},
  publisher = {Springer},
  year = 2019
}

@inproceedings{BMVY2019,
  author = {Laura Bocchi and Maurizio Murgia and Vasco Thudichum Vasconcelos and Nobuko Yoshida},
  title = {{Asynchronous Timed Session Types}},
  booktitle = {28th European Symposium on Programming},
  series = {LNCS},
  volume = {11423},
  pages = {583--610},
  publisher = {Springer},
  doi = "10.1007/978-3-030-17184-1_21",
  year = 2019
}