Principals of Programming Seminar

Friday, May 3, 2019 - 1:00pm to 2:00pm


8102 Gates Hillman Centers


STEPHANIE BALZER, Systems Scientist

Manifest Deadlock-Freedom for Shared Session Types

Shared session types generalize the Curry-Howard correspondence between intuitionistic linear logic and the session-typed pi-calculus with adjoint modalities that mediate between linear and shared session types, giving rise to a programming model where shared channels must be used according to a locking discipline of acquire-release.  While this generalization greatly increases the range of programs that can be written, the gain in expressiveness comes at the cost of deadlock-freedom, a property which holds for many linear session type systems.

In this talk I report on recent work and develop a type system for logically-shared sessions in which types capture not only the interactive behavior of processes but also constrain the order of resources (i.e., shared processes) they may acquire. This type-level information is then used to rule out cyclic dependencies among acquires and synchronization points, resulting in a system that ensures deadlock-free communication for well-typed processes in the presence of shared sessions, higher-order channel passing, and recursive processes.  I illustrate the approach on a series of examples, showing that it rules out deadlocks in circular networks of both shared and linear recursive processes, while still being permissive enough to type concurrent implementations of shared imperative data structures as processes.

Stephanie Balzer is a systems scientist in the POP group currently working on concurrent session-typed programming.  Her work expands linear session types with the possibility of sharing, increasing the range of programs that can be written and introducing nondeterminism and concurrency into session-typed programming.

Event Website:

For More Information, Contact:


Seminar Series