Linear logic has since its inception been viewed as being closely connected to concurrency. However, making this connection explicit has been difficult as it lacked two key features of concurrent programs: the ability to pass messages and the ability to define protocols. Messages consist of data from the sequential world which can be passed along channels from one process to another, while protocols are types which describe patterns of interactions.

The talk will describe the semantics of these facilities in terms of a Curry-Howard-Lambek correspondence between the proof theory (the logic of message passing), the categorical semantics (linear categories), and the term logic (a concurrent programming language).