This is the second of a series of posts based on experiences at POPL (Principles of Programming Languages), 2011, in Austin TX. (Here’s the first.)
I’d stayed up most of the night to prepare my talk, so I skipped the first session of the day to catch up on some sleep. The next session was on separation logic, which had some cool talks: on a separation logic that allows compositional reasoning about atomicity for programs that manipulate concurrent data structures (by folks at Northeastern University); and on modular reasoning for deterministic parallelism (by folks at Cambridge).
Lunch followed, with some pleasant conversations with Stephen Freund (Williams College), Todd Millstein (UC Los Angeles), and Sorin Lerner (UC San Diego).
I sat through the next session fine-tuning my slides, and in the process managing to miss some interesting talks which I have to catch later: on amortized resource analysis; and on symmetric lenses.
The final session of the day was on types (with the final talk being mine). First up was a talk on dynamic multirole session types; Phil Wadler pointed out in his follow-up that an implementation of this system may not allow as must distribution as claimed. Next up was a talk on practical affine types, which showed how to infer some of the associated proof constructs via subtyping (similar to how one moves from sum and product types to union and intersection types). Phil Wadler stressed the importance of syntax in making something “practical”; in particular, he wondered whether the annotations on arrows that affine rules require were indeed practical. On the surface, this seems to be a trivial complaint; but there is definitely something to it, something worth remembering.
Finally, I talked about dynamic type inference of static types. A lot of anticipation had already built up around this talk; we had got top reviews for this paper, and apparently some other groups had been independently trying to solve this problem. The key idea of our paper is to infer types by running tests and logging subtyping constraints along observed paths; what makes it interesting is that we can prove a soundness theorem that is qualified by the coverage of those tests, and we are able to show that the coverage needs to be only linear in the number of functions in a program (although it may be exponential in the maximum number of paths in a function). Such a dynamic analysis technique is especially useful for dynamic languages, where (in our experience and of several others) static analysis is too imprecise. The cool thing about our technique is that while we are precise, we are not “too precise”: our analysis can extract enough abstract information to let us generalize types and predict type errors.
Fortunately, the talk generated a huge amount of interest. Mitch Wand and Matthias Felleisen (Northeastern University) followed up, and I was kept busy long after the talk by others. Sam Tobin-Hochstadt (Northeastern University) and Madan Musuvathi expressed interest in the implementation (which involves wrapping); Sam pointed out the “values-as-proxies” ECMAScript proposal for comparison, and Madan was on the lookout for similar tricks for his concurrency work. Fritz Henglein (University of Copenhagen) pointed out that some of his work from the 90s may be relevant, where he had done the “converse”: static inference of dynamic types. Dave Herman (Mozilla) and I chatted at length on our similar roles at different companies, and discussed the importance of collaborating in the future.
The day ended with Mooly Sagiv (Tel Aviv University) describing the workings of the POPL 2011 PC (which everybody agreed had done a remarkable job), and Phil Wadler presenting the most influential paper award (from POPL 2001) to Samin Ishtiaq and Peter O’Hearn for their work on bunched implications as an assertion language for mutable data structures (a.k.a. separation logic). Peter O’Hearn, in his acceptance speech, recalled that this paper was ready almost half a year before the POPL deadline, but they decided to wait because the best work in programming languages deserves to go to POPL.