I attended PLPV 2010 this past Monday in Madrid, and I think this was the best edition yet of the workshop. I just want to run through the program a little, to give you my take on the talks, all of which were really good (I won’t judge my own talk, of course, but I was happy with how it went).
Invited talk: Gilles Barthe. Gilles spoke on the CertiCrypt project he has been leading for (I believe he said) three years now. The goal of the project, as I understood it from his talk, is to develop computer-checked versions of correctness proofs for cryptographic protocols. As I overheard Tim Sheard saying to Gilles aftewards, this project is really a tour de force. I was completely blown away. Imagine all the incredible engineering effort required to formalize your favorite meta-theorems or program verification problems in Coq (the tool used for CertiCrypt), but replace your standard operational semantics with a probabilistic one, reason about observational equivalence instead of just the operational semantics, and base the whole thing on (I am not remembering the exact name here) probablistic relational Hoare Logic. Get the idea? They have had to develop significant new formal theories here, which are richer and more complex than the ones I at least am used to thinking about — and I don’t think those are trivial to begin with! Also, the talk was really good, with a great balance of higher level motivation and detailed theory. Again, really really great.
Stefan Monnier. The creative and surprising talks just continued, as Stefan told us about how to translate a dependently typed language (the Calculus of Constructions, to be exact) into a language with only singleton types. I did not quite understand the significance of this at first, but the point is that the target language of his translation enjoys a true phase-distinction: singleton types are indexed by compile-time expressions, which have no computational relevance. In contrast, the full-spectrum dependently typed source language allows types to depend on run-time expressions. So the interesting point was that this dependence can be eliminated in favor of dependence only on compile-time expressions. I still have to digest this further, but it was an intriguing talk, and the technical development is very pleasing (particularly the definition of the translation).
Matthew Danish. Matthew gave a very clear and understandable talk on implementing parts of an OS in ATS, Hongwei Xi’s dependently typed programming language. He showed how the type system can enforce unique references to kernel data structures using linear types, and introduced a very nice ATS construct for saying that a resource is not consumed, but its type is updated (written something like x : T >> T’). That idiom would be very nice to have in my Guru language…
Stephanie Balzer. Stephanie’s was the first (but certainly not the last) talk of the day to take the workshop into new technical territory, with relationship-based programming. The basic idea (as I understood it from her talk) is to reify the dependences and connections between classes as additional entities called relationships. So in fact, entity classes have no members referring to other entities. All connections are embodied in relationship instances. I am definitely still digesting this idea, but it makes a lot of sense that making dependencies explicit could help verification. And that is exactly what Stephanie describing in this very clear and well-presented talk. One does not need multi-object invariants in Rumer (her language), because all state which could be interdependent is located in a single relationship class.
Chris Casinghino. Chris introduced to the wonders of doubly generic programming: both datatype generic (where programs are not parametrically polymorphic, but instead, are defined inductively on the structure of the type in question), and arity generic. In fact, he showed how arity generic falls right out of the natural general formalization of datatype generic. It is really appealing to attain this level of abstraction. While I couldn’t reproduce the technical ideas at this point without looking again at the paper, the presentation was quite clear and enjoyable.
Daniel Seidel. Daniel also led the workshop into intriguingly new territory, by talking about free theorems (that is, those derived by parametricity for parametrically polymorphic programs) for functional logic programs. This was very interesting to consider, for someone like myself who is not so familiar with the functional logic programming paradigm. Daniel explained how nondeterministic choice — where we can have terms like “3 ? 4” meaning a value that is nondeterministically chosen to be either 3 or 4 — requires revision of the free theorems that one can derive; essentially, the theorems need to be weakened to allow for one term having a subset of the nondeterministically computed results of the other. With some nondeterministic features, a further restriction was required to get any free theorem at all. A very nice talk, that fit very well with PLPV’s goal to include a stimulating variety of topics under the banner of language-based verification.
Jan Vitek. Jan gave an inspiring call to arms for language-based verification researchers to take up verification of real-time programs, particularly real-time Java programs. He explained that this is an area where industry and military procurement is open to new languages and new methods; they are willing to accept restrictions on how programs can be written; and the demand is very great for real solutions, that compromise neither reliability, performance, nor scalability. He presented a collection of real-time Java benchmarks, some of which use a real-time garbage collector, and others scoped memory. The paper highlights several important properties (e.g., absence of uncaught exceptions, including null pointer dereference; memory allocation rate; etc.).
Stephanie Weirich also gave a brief overview of the current status of the Trellys project, which she, Tim Sheard, and I are leading up. The goal is to design a new dependently typed programming language, which includes general recursion and very expressive polymorphism, but retains a fragment which is sound as a logic (that is, where programs of type A -> B can be soundly viewed as proofs of the formula A -> B). The three of us, Bruno Barras, and Chris Casinghino met the day before PLPV at IMDEA Software in Madrid to hash through a bunch of technical ideas on the Trellys core language. I’ll have to talk about that, though, at another time, since this post is too long already.