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:

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.

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

Your obt.pdf link looks broken there Neel...

ReplyDeleteThanks -- the link should be working now.

ReplyDelete