Session Types and Higher-Order Concurrency

Jorge A. Pérez

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.

Based on joint works with Alen Arslanagic, Dimitris Kouzapas, and Nobuko Yoshida.

---

Previous: Jesper Cockx | Dependent pattern matching: theory and implementation
Next: Eelco Visser | What is PL research?