Session Types, Depending on the Traffic

A key feature of session types is that they provide, by their "choice" constructs, the means for the later structure of a protocol to be determined by earlier signals in the protocol. That makes a type theorist like me think of Sigma (dependent pair) types and Pi (dependent function) types, as sending or receiving (respectively) a signal, then proceeding in accordance with some interpretation of that signal. In this talk, I'll use induction-recursion, the type theorist's go-to tool for building universes of dependent types, to develop a notion of dependent two-party session type for non-recursive protocols. I'll show how to compute compositionally the inherently higher-order types for the behavioural strategies of the two parties, but I shall make sure that the protocol does not depend on those strategies, rather only on the first-order signal traffic produced by executing those strategies. If time permits, I'll explore, not without hope, the obstacles which arise when we try to add recursion, or when we have more than two parties.

Note the nonstandard location; if we turn out to have too many people for the room, we'll move to LTB. Also, this talk will not be on Zoom (since it will be whiteboard-based).