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.

Integrating Linear and Dependent Types at POPL 2015

I'm very happy to announce that Integrating Linear and Dependent Types will appear at POPL 2015! The link above goes to the final version, which (at the behest of the reviewers) has been significantly expanded from the original submission. (Added up, the total length of the reviews was almost half the length of the submission, which says something about the degree of care taken in the process.)

Also, Jeremy Yallop has put together a web page with links to many of the POPL 2015 papers. Some of the freely available ones (as of this writing) which catch my eye are:

• Formal verification of a C static analyzer, by Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy and David Pichardie

  Astrée is one of the big success stories in verification. Apparently they are building a provably correct(!) version.

• Space-Efficient Manifest Contracts, by Michael Greenberg

  One of the big difficulties in applying contract checking to functional programming is that it breaks tail call optimization. This paper says that you can do it without breaking TCO, which is (a) a real breakthrough, and (b) probably has all kinds of applications.

• Functors are type refinement systems, by Paul-André Melliès and Noam Zeilberger

  I knew fibrations were important for characterizing inductive definitions in type theory, parametricity, and the semantics of dependent types. Apparently they are also important for characterizing refinement types.

• Programming up to Congruence, by Vilhelm Sjöberg and Stephanie Weirich

  This is a dependent type theory which works up the congruence closure of the equality hypotheses in the context, rather than using a judgmental equality. The treatment of equality is the central problem in the design of dependently typed languages, so it's nice to see exploration of the design space. (This approach reminds me a bit of the Girard/Schroeder-Heister equality rule, which semi-secretly underpins GADTs.)