Everyone is welcome to attend the SWAT lecture of Jorge A. Pérez, Associate Professor in Software Foundations at the Bernoulli Institute, University of Groningen.
Title: Session Types and Higher-Order Concurrency
Abstract:
Session types are a type-based approach for communication correctness in message-passing, concurrent programs: a session type specifies what should be exchanged along a communication channel and when. Session types have been originally developed as typing disciplines for processes in the pi-calculus, the paradigmatic calculus of interaction and concurrency.
While there is substantial value in looking into session types for the pi-calculus, it is also insightful to investigate them in the context of core programming calculi that feature a closer link with (functional) programming languages. To this end, we have studied HO, a minimal calculus for higher-order concurrency and sessions. As in the pi-calculus, HO features message-passing concurrency governed by session types; unlike the pi-calculus, the values exchanged by HO processes are abstractions (functions from names to processes).
In this talk, I will discuss two key expressiveness results for HO processes with session types. First, HO and the session pi-calculus are equally expressible: one language can be encoded into the other, up to tight behavioral equivalences. Second, there exists a small fragment of standard session types that suffices to represent all typable HO processes. Combined, these two results provide compelling evidence of the expressive power and convenience of HO as a compact blend of sessions and higher-order concurrency.
