Asynchronous timed session types: from duality to time-sensitive processes

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