Groupe de travail, 7 mars 2013
Exposés
 10:30: Subashis Chakraborty (Calgary), The proof theory of message passing with protocols

Sequential programs are connected through the λcalculus by the CurryHowardLambek isomorphism to intuitionistic proofs and cartesian closed category. The CurryHoward 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 twosided proof theory of cut elimination and described a categorical semantics of the system. In this talk, we will describe this twotier 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.