\ (\) LL: Reconciling Linear Logic, the \ (\) -calculus, and their Metatheory

The Curry-Howard correspondence between natural deduction and the \ (\) -calculus has been a tremendous source of inspiration for typed functional languages. Initiated by Abramsky 1994, the Proofs as Processes agenda seeks a similar foundation for typed concurrent languages, in terms of a connection between linear logic Girard 1987 and and the \ (\) -calculus Milner et al. 1992. Recent advances established solid correspondences at the levels of types and syntax. Linear propositions correspond to session types Caires and Pfenning 2010; Wadler 2014 – types that prescribe the observable communication behaviour of processes Honda 1993 – and the fundamental operators of the \ (\) -calculus correspond to rules in linear logic formulated with hypersequents Carbone et al. 2018; Kokke et al. 2019; Montesi and Peressotti 2018. But at the level of semantics and metatheory, the situation remains unclear. The semantics and behavioural theory from previous work do not respect the prefix operator of the \ (\) -calculus. The operational semantics of session types has not been reconstructed yet, and as a consequence the hallmark result of session types (session fidelity) has not been formulated and proven for Proofs as Processes. In this article, we carefully evolve the design of Proofs as Processes by applying a dialgebraic view of labelled transition systems and their homomorphisms to the proof theory of linear logic Ciancia 2013. The resulting calculus, called \ (\) LL, ties previous loose ends and further exhibits a comprehensive metatheory that connects the proof theory of linear logic to the behavioural theory of the \ (\) -calculus. Our development clarifies the properties guaranteed by linear logic on the observable behaviour of processes. It also includes a new principle for reasoning about the internal work performed by processes, which we use to establish the first deadlock-freedom and productivity results for processes with observable actions typed with linear logic.