Home » forums » LtU Forum

The logic of communicating on channels

J.R.B. Cockett and C.A. Pastro. A language for multiplicative-additive linear logic, Electronic Notes in Theoretical Computer Science 122.
J.R.B. Cockett and R.A.G. Seely. Finite sum-product logic, Theory and Applications of Categories, Vol. 8, No. 5.

Last evening I had the opportunity to see Professor Robin Cockett (University of Calgary) give a talk about the logic of communicating processes.

Of the talk:

Abstract: Communication along a channel between two processes is governed by a protocol which dictates what sort of messages can be sent and received at any given time. A very basic question is: when are two processes which are attached to a number of such channels indistinguishable?

One way to answer this question is to ask whether this situation is actually the proof theory of some logic. A positive answer to this places the equivalence on an algebraic footing and allows communication to be viewed as a cut-elimination process.

Proof theories of this sort are equivalent to categorical "doctrines" and it turns out that the logic of communicating along channels is a very very basic categorical doctrine which, nonetheless, has only recently received significant attention. It is the categorical doctrine of free products and coproducts and disturbingly little is known about it!

The talk will discuss these connections and some of what is known.

As it is fairly obviously related to the subjects under discussion here, I though I'd take the opportunity to make my first real post.

By Thomas Sutton at 2005-05-13 02:14 | LtU Forum | previous forum topic | next forum topic | other blogs | 2409 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Very practical

The first paper was one of the three I used recently while designing a little language for data processing - it didn't contribute directly, but helped me to understand other papers better.

The second paper looks promising - I was missing something like this when studying computability logic.

I am still playing with idea to design a concurrent typed PL based on some logic, and this one can be a good candidate (I have to read past page 5, though :) ).

[on edit: aha, if I am right, the game semantics for this logic has only choices in form of (co)products, but no parallel subgames... Have to think about it more... Probably I need to bump ΣΠ-polycategories, additive linear logic, and process semantics up my (re)reading list. Currently, A calculus of circular proofs and its categorical semantics is higher :)]

By Andris Birkmanis at Fri, 2005-05-13 08:08 | login or register to post comments