Subashis Chakraborty (Calgary), The proof theory of message passing with protocols



Sequential programs are connected through the λ-calculus by the Curry-Howard-Lambek isomorphism to intuitionistic proofs and cartesian closed category. The Curry-Howard isomorphism allows proofs to be viewed as programs and propositions as types. But what is the proof theory of concurrent programs? Message passing is a key element of concurrent programming. In the paper The Logic of Message Passing (2007), Cockett and Pastro showed how message passing could be accomodated in the proof theoretic framework for concurrency. They used the two-sided proof theory of cut elimination and described a categorical semantics of the system. In this talk, we will describe this two-tier message passing logic. We will focus on providing an intuition for the system. The cut elimination of the system provides an operational semantics, which we shall illustrate with examples. We will also go through some examples to show how protocols work in this system, where protocols actually datatype in the process (concurrent) world.