Back from POPL, forward to AGDA

I arrived back in Pittsburgh yesterday after a week at POPL and related workshops in San Francisco. Modulo the stress of having to prepare my presentation for the last day, it was a lot of fun! Heard lots of interesting talks, and had many interesting conversations. The highlight was probably Conor McBride's performance of "Clowns to the left of me, jokers to the right" ("I watch Olivier Danvy as he circles the room with a knife, threatening to defunctionalize my continuation"), but I also really enjoyed Janis Voigtlaender's talk, "Much Ado about Two". Knuth's 0-1 principle states that any oblivious sorting algorithm can be verified correct simply by testing it on arrays of 0s and 1s. Voigtlaender proved an analogous result for parallel prefix sort: correctness can be verified simply by testing arrays of 0s, 1s, and 2s. The neat thing is that the result can be obtained almost as a "free theorem", i.e. by proving a few simple combinatorial properties and applying parametricity. This paper also seems to me in a similar spirit as Martín Escardó's seemingly impossible functional programs and Kevin Watkin's 98-line proof of Conway's Cosmological Theorem─very clever uses of Haskell to reduce a seemingly infinite search space to a finite one. These sort of results make me feel optimisic about the future.

Another thing that makes me feel optimistic: Agda2. Dan Licata and I had a coding session today to try to translate focusing-with-higher-order-rules into Agda, and it seems almost perfectly suited. Dependent pattern-matching and unicode: a killer combination. I will try to post more about this in the next few days.