SWAT seminar: Jorge A. Pérez (Universiteit Groningen)

Everyone is welcome to attend the SWAT lecture of Jorge A. Pérez, with the title 'Session Types and Higher-Order Concurrency'.
  • What Software Analysis & Transformation English
  • When 01-11-2019 from 11:00 to 12:00 (Europe/Amsterdam / UTC100)
  • Where Room L120 at CWI, Science Park 123 in Amsterdam
  • Add event to calendar iCal

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

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.