Existing work on timed session types leaves a number of open problems. On the practical side, they are based on simple abstractions, and do not capture : (a) primitives used in the real world, like blocking receive primitives (with and without timeout), or (b) realistic abstractions for time consuming actions with variable, yet bound, durations. On the theoretical side, a notion of duality for in asynchronous timed interaction is missing. Duality would provide an answer to the question: "Given a timed asynchronous protocol for an endpoint, what is its natural counter-part?". As I will show, this is a non-trivial question, and a naive extension of duality with asynchrony and time does not ensure the usual desirable properties of well-typed programs. I will present foundations of timed asynchronous duality, and provide a theory of timed asynchronous session types for a realistic calculus that caters for (a) and (b). Well-typedness guarantees absence of communication mismatching (aka communication safety) and punctuality (i.e., messages will be sent/received within the specified time-frames).
Cornwallis South West,
University of Kent,