PoP Seminar Talk
A Propositions-as-Sessions Interpretation of Bunched Implications
Bas van den Heuvel,
PhD student at the Bernoulli Institute, University of Groningen
Monday, 28 November, 2022; 3:30pm
Host: Stephanie Balzer
The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic.
In this presentation I introduce a new point in the design space of session type systems for message-passing concurrent programs. We identify O’Hearn and Pym’s Logic of Bunched Implications (BI) as a fruitful basis for an interpretation of the logic as a concurrent programming language. This leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic. We introduce a new π-calculus with sessions, called πBI; its most salient feature is a construct called spawn, which expresses new forms of sharing that are induced by structural principles in BI. We illustrate the expressiveness of πBI and lay out its fundamental theory: type preservation, deadlock-freedom, and weak normalization results for well-typed processes; an operationally sound and complete typed encoding of an affine λ-calculus; and a non-interference result for access of resources.
Bas van den Heuvel is a PhD student at the University of Groningen in The Netherlands. His research is on the foundations of correctness for communicating software. The focus is on static correctness using session types, but dynamic correctness using monitoring and model checking are also explored. A major theme in this work is connections to logic, reaching toward more canonical and less complex approaches.