*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.

## No comments:

Post a Comment