Curry-Howard for GUIs: Or, User Interfaces via Linear Temporal, Classical Linear Logic

Together with Jennifer Paykin and Steve Zdancewic, we have written a short note about the next phase of the long project to make GUI programming intellectually manageable.

Essentially, the idea is that the natural language of graphical user interfaces is $\pi$-calculus, typed using classical linear logic (plus some temporal modalities). Furthermore, we think that the implementation strategy of callbacks and event loops can be understood in terms of Paul-Andre Mellies' tensorial logic. So we think we can:

1. Explain how there are secretly beautiful logical abstractions inside the apparent horror of windowing toolkits;
2. Illustrate how to write higher-order programs which automatically maintain complex imperative invariants, and
3. Write some Javascript programs which we think are actually $\pi$-calculus terms in disguise.

You can download the draft here. If you want to read something with more theorems than this note, I'd suggest looking at Jennifer and Steve's paper about their Linear/Producer/Consumer calculus for CLL.