Message Theories (project proposal)

In my PhD thesis, I developed a bit a notion of “message theory”. Every symmetric monoidal category (every process theory) gives rise to a free message theory. Every message theory has an underlying process theory. This induces an adjunction between message theories and symmetric monoidal categories. Message theories have a good combinatorial characterization, but it is unclear to me how to classify them categorically.

message-theory

The syntax for message theories is very succint: a shuffling operation that sequences programs, linking and spawning channels, and a no-operation. One could create a simple concurrent programming language over these primitives. Its semantics would stand in contrast to linear logic-based approaches to concurrency.

Research proposal. To identify categorical structures similar to message theories (duoidal categories, posetally-enriched monoidal categories, duoidally-graded monoidal categories), and to develop programming languages using message theories. To extend the theory without breaking its combinatorial properties.

References.