POPL'09: day three

Today kicked off with a keynote from my old friend, Alex Simpson, who spoke on "linear types for computational effects". I *really* enjoyed Alex's talk - but there again, I did write my thesis on linear types, and spent a couple of years on a postdoc position trying to doing something similar :-)

Alex has, I think, actually solved the problem that we were trying to sort out but too dim to make any serious progress, i.e. a universal metalanguage for cbv and cbn. In those days we hoped "pure" linear types would suffice. They don't quite work. What Alex has now done is figured out which bit of them you need.

Alex starts with not the computational lambda calculus, but an interesting variant: Filinski's effect calculus. This makes a similar distinction of value and computation, but actually has two grammars of types. Alex then "enriches" the calculus with linear types, but does this using a Girardian "stoup". A really nice feature is that Alex has a decent, computational explanation of the stoup: a term with a stoup is an evaluation context, i.e. it's a linear function that "immediately" evaluates the computation that is put in the hole. [As an aside: Andy Pitts and I had fiddled with evaluation contexts and Lily; for a while we had an evaluation relation that internalized the evaluation context using linear functions. Very cool, but too confusing so we dropped it.]

Anyhow, Alex has a very natural calculus whose induced monad is commutative - the big problem with early linear work was that the induced monad was non-commutative. As there are very few non-commutative monads, this was a very sore point.

So, I really liked Alex's talk - I think there's some very nice more operational work to be done here. I shall be waiting for Alex to publish his slides next week - maybe I'll end up taking a trip to Edinburgh sometime soon...

I then enjoyed three talks on program logics. Nearest to my heart was James Brotherston's talk on a classical version of BI. It's highly non-trivial to find a classical version of BI that doesn't collapse everything, so it was sweet to see it all work out.

I also enjoyed Benoit's talk on open existential types. Essentially they have deconstructed the existential operators, so (in my view) they are more like module-like operators. However, the resulting calculus is (also in my view) much simpler than any module calculus I have seen. Benoit rushed through some of the details, so I look forward to checking this paper out.

Neel did a great job describing his work on focusing and pattern matching, especially as he faced not one but two laptop crashes in his talk. Poor guy.

POPL ended with a great talk by Chris Hawblitzel. Chris has implemented a couple of garbage collectors in BoogiePL; had then verified by the Boogie/Z3 infrastructure, and then he has spliced them into the Bartok compiler. Wow! You wouldn't have thought it possible - so this was a nice way to end POPL.

I ended up having a nice walk along the river with Lars and Alin (after we were stood up by Andrew and Claudio!). We went for a beer at one of the many bars and then had a nice meal at one of the "Italian" restaurants (Calamari followed by rack of veal). [Unfortunately I think the chap who was sneezing over me in PLPV has passed on his bug, so I had to go to bed early and have a bad night's sleep :-(]