A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency

TL;DR

This paper introduces a novel session type system based on Bunched Implications logic, offering a new approach to resource sharing and concurrency in message-passing programs, with formal guarantees and expressive power.

Contribution

It presents ${ m ext{ extpi}}$BI, a new ${ m ext{ extpi}}$-calculus with sessions based on BI logic, differing from Linear Logic-based systems, and establishes its fundamental properties.

Findings

Type preservation and deadlock-freedom for ${ m ext{ extpi}}$BI processes

An encoding of affine ${ m ext{ extpi}}$-calculus into ${ m ext{ extpi}}$BI

A non-interference property for resource access

Abstract

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 paper, we investigate 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 ${\pi}$-calculus with sessions, called ${\pi}$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 ${\pi}$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 ${\lambda}$-calculus; and a non-interference result for access of resources.