March 17th at 17:00, in Zoom
Type systems are a useful tool to prevent programmers from making obvious mistakes, but they are generally quite limited in what they can describe. We've taken a look at a session types, a type system aimed at describing communication protocols, and checking that programs adhere to these protocols. Where previous work on session types has treated them as syntactical objects, we find that protocols have a natural notion of state and characterize them as coalgebras, i.e., state-based machines. In doing so, we retrieve natural definitions for type-equivalence, subtyping and duality of types as coinductive relations between states. In my talk I'll explain what session types are and present our syntax-free description of protocols as states of a coalgebra (without assuming prior knowledge of coalgebras).