Last week I discussed some newly-explored proof-theoretic relationships between reasoning about process calculi and substructural logics, and vaguely mentioned some other programming models that I wanted to compare. Since then, I think I've come up with a way to phrase my research objective with this project: to relate the programming and reasoning methodologies surrounding interactivity through a common medium of proof theory.

That's not a thesis statement, but I figure it's better than "*waves hands excitedly* interactivity! Processes! Linear logic! Focusing!"

Anyway. What I've done so far has given me more questions than answers, but I like the questions a lot. The first of these questions I want to discuss in this post is "How can proof theory capture an appropriate notion of broadcast message replication?" To explain what I mean by that, I'll describe an example which I think captures some common interactive communication patterns.

Lights O…

That's not a thesis statement, but I figure it's better than "*waves hands excitedly* interactivity! Processes! Linear logic! Focusing!"

Anyway. What I've done so far has given me more questions than answers, but I like the questions a lot. The first of these questions I want to discuss in this post is "How can proof theory capture an appropriate notion of broadcast message replication?" To explain what I mean by that, I'll describe an example which I think captures some common interactive communication patterns.

Lights O…