I am in Copenhagen for ICFP, in very good company (including a large part of Gallium). There is a lot to do and just listening to talks and speaking to people takes a large amount of time and energy.

On Sunday, I attended the HOPE workshop, Higher-Order Programming with Effects; I would very much have liked to attend LFMTP and WGP as well, but you can only be in one place… (I hope to also write a bit about the talks at HOPE, but I need to first see if the authors have their slides online…)

Monday was the beginning of the main conference. After an explosive keynote by Conor, we had a lot of great talks. I originally planned to skip one of the sessions to go to the swimming-pool and preserve some of my mental sanity for the next few days, but couldn’t come to doing it because it all looked too tempting. Here are a few highlights.

(I also had great experiences with Danish food, in particular the sweet marinated herring. At lunch I had a great discussion with Jonathan and Scott Kilpatrick, a student of Derek Dreyer that is working on formal approches of Haskell package management inspired from ML module systems.)

Agda-curious? An Exploration of Programming with Dependent Types,

keynote by Conor McBride

Conor made a dramatic keynote as he does well. It was fun, it was interesting, it was surprisingly practical and it all worked well. He wrote a compiler from a simple arithmetic expression language to a simple stack language in Agda, and then shown how he could gradually refine the type of the stack items to bake in correctness arguments: that the size of the stack is respected (evaluating the result of compiling an expression only adds one element on the stack), that the type of the stack items are correct, and finally that compilation preserves the expression’s semantics.

I think what was most impressive to the part of the audience not familiar with Agda was the demonstration of its interactive programming mode, all in Emacs glory, with hole-filling and single-keystroke-dependent-case-splitting. This strongly support Conor’s vision that we should use types to help us write programs, not just debug or maintain them. I regretted the absence of his typical colorful hand-drawn overlays, but admittedly proof assistants don’t run very well on pen&plastic.

Conor also made a running comment on an opposition in the proof assistants community between people that advocated writing programs with simple types (eg. corresponding to ML or System F), and separately proving properties about them, and people that advocate writing richly, dependently typed programs that carry their own correctness proofs. He believes in “a mixed economy” where everyone is free to choose a point in the continuum between those two opposites, and suggests that we should actively support both styles.

Verified Heap Theorem Prover with Paramodulation, by Gordon Stewart

(Join work with Lennart Beringer and Andrew Appel)

The talk was very strong, with both crisp ideas of the problem domain (which I don’t know much about) and well-done, easy to assess empirical results. In short, they wrote an automated prover for separation logic statement similar to an existing solver, but their one is entirely written in Coq, with of course a correctness proof.

In the SAT/SMT community, the histories of “we took this paper and implemented in Coq” are often not that good: a lot of the performances come from low-level hack that are hard to compete with in a sane language. Their story here is much better, as they are competitive with existing, specialized solvers, thanks to the use of a state-of-the-art algorithm and nice work on profiling and optimizing the Coq program – executed through extraction to OCaml.

The small detail : they presented a range of optimizations they did on the code (from micro-optimizations like extraction to OCaml’s int31 native integers to high-level algorithmic changes) and for each gave not only the runtime speedup, but also the blowup in code size resulting from the change. They ended up 22 times faster than their prototype, but also with 5 times more code. I liked having both numbers and think we should do that more often.

Superficially Substrucural logic, by Neelakantan Krishnaswami

(Joint work with Aaron Turon, Derek Dreyer and Deepak Garg)

This works build upon the ideas of separation logic, a reasoning technique for imperative program that allows the programmer to reason about fragments in isolation, and easily compose two pieces that affect distinct fragments. In the last few years, people have worked on generalizing this idea to other kind of resources, not just the memory heap but also possibly output files, key/value pairs in a shared hash table, segments of an array shared between workers, etc. The idea is that any monoid, in a linear type theory, can be reasoned over as a separated resource.

Neelk gave a clear presentation of their work, which allows users to define their own resources in their program and reason on all kind of resources at once – instead of having one distinct logic for each form of resource. It uses features from the typed programmer toolset such as existential types to make this construction possible in programs.

Operational Semantics Using the Partiality Monad, by Nils Anders Danielsson

Nils gave a well-executed talk on using a “Partiality Monad” to represent and reason about non-terminating programs in Agda. He started from a “denotational interpreter” for the untyped lambda-calculus, with a naive non-typable version, and then a simple modification of it to capture both type failure at application and the potential for non-termination. He then went on to show how we could state properties of the evaluator and derived implementations (an abstract machine counterpart of it) in a natural way that still captured all we want to say.

For example, you don’t want to only say that “if my lambda-term terminates with a value, the compiled abstract bytecode terminates with the same value”: you probably want to capture as well that non-termination of the lambda-term should incur non-termination of the abstract machine counterpart. Nils manages to capture both those ideas in single, natural statement.

The talk was very well executed but appealed most, I suppose, to people familiar with those issues of stating properties about impure programs – a problematic that is very important in some of the work on Compcert, for example.