Computer Science Department
School of Computer Science, Carnegie Mellon University


Manifest Sharing with Session Types

Stephanie Balzer, Frank Pfenning

March 2017


Superseded by CMU-CS-17-106R
June 2017

Keywords: Linear logic, Curry-Howard isomorphism, session types, message-passing concurrency, sharing

Session-typed languages building on the Curry-Howard isomorphism between linear logic and session-typed communication guarantee session fidelity and deadlock freedom. Unfortunately, these strong guarantees exclude many naturally occurring programming patterns pertaining to shared resources. In this paper, we introduce sharing into a session-typed language where types are stratified into linear and shared layers with modal operators connecting the layers. The resulting language retains session fidelity but not the absence of deadlocks, which can arise from contention for shared processes. We illustrate our language on various examples, such as the dining philosophers problem, and show that sharing recovers the computational power of the untyped asynchronous π-calculus.

70 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by