PLPV 2011 took place this past Saturday in Austin, Texas, as a POPL-affiliated event. I was quite happy with the meeting. I got to meet Nik Swamy for the first time, whom I had been hoping to get to talk to about the dependently and affinely typed programming language Fine that he is developing with his collaborators Juan Chen (whom I was happy to meet again after many years since I made her acquaintance at Princeton, where she was finishing as a student and I was visiting Andrew Appel for some weeks in the summer, maybe 2004 — I forget), and Johannes Borgstrom, whom I was very pleased to meet for the first time. Their talk on how to allow subset types to refer to affine (use-at-most-once) values without counting such references as uses was quite interesting, and just confirmed for me the value of the work we have been doing on the Trellys project on Freedom of Speech. This is a language feature which supports a use/mention distinction: terms are allowed to mention or refer to other terms without those references counting as uses of the other terms. In our case, we want to allow normalizing proof terms to refer to possibly non-normalizing program terms without losing the normalization property for proofs. This is similar to the issue in Fine, where one naturally wishes to formulate post-conditions of functions in terms of affine inputs, without having occurrences of those inputs in the statement of the post-condition count as uses of the inputs (which, after all, are limited to at most one use).
The rest of PLPV was also quite good, in my opinion. J Moore gave an inspiring (for our better angels, depressing for our worse) overview of ACL2, and had just some really amazing demos of what ACL2 can deduce automatically. Yes, those results do depend on a lot of already proved lemmas, but still: I watched things I have literally spent weeks proving in Guru get proved automatically by ACL2 in milliseconds. Sigh. David Walker explained a really nice abstraction for incorporating the power of separation logic into traditional Hoare logic, without the need for a theorem prover for separation logic. Basically, the idea is to allow the programmer to specify the separation of the heap into heaplets. A critical facet of this abstraction is an operation for moving a location from one heaplet to another. That seemed like quite a cool idea. Gordon Stewart from Princeton talked about an impressive sounding project to support (I hope I don’t get this wrong) machine-checked soundness proofs for separation logic for Cminor, one of the languages of Xavier Leroy’s Compcert verified compiler. Derek Bronish spoke elegantly about a particular verification challenge problem, namely specifying, implementing, and verifiying a data structure implementing maps. I had not met Edwin Brady before, though knew some of his work in compilation for dependently typed programming languages. He gave an inspiring talk on his dependently typed language Idris (which is named for the dragon which grew up inside Ivar the Engine’s boiler in a popular British cartoon, he told me later), and argued convincingly that dependent types could be well used for accurate programming with binary file formats (since dependent types can express the dependencies between different fields of a packet header, for example). Meera Sreedhar of UT Dallas gave an informative and well presented talk on verification of inlined-reference monitors (a problem coming from the security domain, where for efficiency, one wishes to inline security monitors directly with the code they are supposed to watch) as a challenge problem. Finally, Chris Casinghino from U. Penn. did a great job summarizing the state of our Trellys project, and fielding some very good questions from the audience about our language design to date.
So that’s a little update from PLPV 2011, and here’s to PLPV 2012!