This is the first of a series of posts based on experiences at POPL (Principles of Programming Languages), 2011, in Austin TX.
Tom Ball (MSR Redmond) launched proceedings with his usual flair and some cool slides on POPL 2011 records.
The first session of the day was an invited talk by Xavier Leroy (INRIA Rocquencourt). I’ve known Xavier by face and reputation since the summer of 2002, when I was an intern in the Cristal group (working with Gérard Huet). Xavier talked about how his and others’ work on certified compilers over the years has ensured that the verification of realistic compilers is now well within reach. The next frontier is certified static analyzers, on which he provided some hope of progress. Finally, he called for more verification work around floating point (FP); of particular interest was a list of unfounded compiler optimizations around FP, which Alex Aiken (Stanford) extended in his follow-up with the curious fact that FP addition is non-commutative in C. Overall, a thoroughly educational talk, littered with memorable quotes:
“Old pots make tasty soups.”
“It makes me nervous to fly an airplane since I know they are designed using floating-point arithmetic.”
The next session was on memory models, which featured two excellent talks (by folks at University of Cambridge): on certified compilation of C under an exposed x86 memory model; and on semantics and proofs for C++ concurrency.
I skipped the next session; part of the typical POPL experience is being drawn into extended conversations with old and new friends on “stuff.” I was particularly surprised to find my undergraduate advisor on the loose.
The final session of the day was on types. Phil Wadler (University of Edinburgh) gave a hugely entertaining talk (in his inimitable style) on blames for the polymorphic lambda calculus. Dimitrios Vytiniotis (MSR Cambridge) showed a way of resolving the tension between generative type abstraction and type-level computation; Karl Crary (CMU) in his follow-up seemed to suggest that there might be a cleaner way.
In the evening, Tom Ball and co. did live jazz, much beer and scotch flowed, and the night ended with an interesting dinner: amidst some very lively conversations with Samin Ishtiaq (MSR Cambridge), Ranjit Jhala (UC San Diego), Cormac Flanagan (UC Santa Cruz), Madan Musuvathi (MSR Redmond), Eran Yahav (IBM Research NY and Technion Institute of Technology Haifa), and many others.