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 talk, I report on our work on manifest sharing, which introduces sharing into a session-typed language such that 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. Our language can accommodate examples, such as producer-consumer queues and dining philosophers, that could previously not be expressed with linear session types alone, including a translation of the untyped asynchronous pi-calculus into our language.
Stephanie Balzer is a Systems Scientist in the POP group, working with Frank Pfenning on Session Types. Prior to joining the POP group, Stephanie was a postdoc with Jonathan Aldrich. Stephanie received her PhD from ETH Zurich, under the supervision of Thomas Gross, for the development of the programming language Rumer and its modular, invariant-based verification technique.