MFPS 2011 is winding down. It turned out to be a very enjoyable conference — I understood many more of the talks than I expected. Aside from the *many* excellent separation logic talks, the standouts for me were:

**Neel Krishnaswami**'s talk on higher-order FRP, which amongst other things introduced an elegant, practical type system for avoiding space leaks.

**Stephanie Weirich**'s talk on the Trellys project, which attempts to make dependent types practical for *programming*, not just for proof assistants. You begin with a full-blown programming language (including full recursion and other effects), which is logically inconsistent. Then you use a separate typing judgment to pick out a “logical” sublanguage, which *does* coincide with a logic via Curry-Howard. There are many interesting design choices about how these two languages relate, and how to achieve proof irrelevance at the right points. The upshot is that dependent types can be introduced gradually into a program.

**Alex Simpson**'s talk about verification of probabilistic systems. The talk began with a summarization of his previous work on a sequent calculus for proving mu-calculus properties about CCS processes. I had previously seen this work, but he explained it in a way that was new to me: after giving a game semantics for mu-calculus formulas, he proceeded to motivate all of the sequent calculus rules via this game semantics — in an almost mechanical fashion. This seems like a very useful technique.

**Vasileios Koutavas**'s talk showing how any of several naive extensions to applicative bisimulation fail to be sound, via a series of counterexamples. The conclusion in the end is that you really do need the machinery of environmental bisimulation to handle many interesting language features. I suspect the paper will serve as a great way to understand the subtleties of these language features, and I plan to read it soon.

Aside from watching these wonderful talks, I also gave a presentation of my own, about new full abstraction results for the pi-calculus using ideas from separation logic. Here’s the abstract:

Read More