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

### Programme

- 7 mars 2013, 10:30 - 12:00

### Résumé

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.