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.)