Message passing logic

Whats in these talks? Introduction to message passing logic, graphical calculus of linearly distributive categories, linear actegories, free cornering and resource transducers.

This talk was the first part of two-days tutorial at the 30th Foundational Methods in Computer Science Workshop (FMCS 2023) held at Mt. Allison University, Sackville, Canada in July 2023. 

Abstract: 

Cockett and Pastro introduced two-tiered ‘Message Passing Logic’ in order to develop a type theory for concurrent programs with message passing as the communication primitive. The motivation was to allow one to guarantee certain formal properties of concurrent programs such as deadlock and livelock avoidance, which is not possible using the current programming technologies. Current programming languages lack such features because concurrency constructs are embedded in the sequential core without a formal underpinning. The categorical logic behind the machinery introduced by Cockett and Pastro is based on monoidal categories acting on linearly distributive categories with the proof theory given by multi categories acting on poly categories, and is called a linear actegory. Chad Nester introduced resource transducers for concurrent process histories which is a toy model of linear actegories. This talk introduces Cockett and Pastro’s message passing logic and Nester’s resource transducers which is a toy model of this logic.