One Done, Two Submitted

One paper finished, two new ones submitted.

Productive Coprogramming

Conor and I have just submitted the final version of "Productive Coprogramming with Guarded Recursion" to the publishers. Looking forward to ICFP in Boston!

Pair of Papers Pertaining to Parametricity

Dependent Types

With Neil and Patty, we've constructed a relationally parametric model of impredicative and predicative dependent type theories. Highlights: (1) we prove the existence of initial algebras for all indexed functors; and *(2) the model is constructed using reflexive graphs, a kind of cut-down version of groupoids.

Classical Mechanics

Just by myself, I've also done a paper on using relational parametricity to prove symmetry properties of Lagrangians in classical mechanics, so that you can derive conservation laws via Noether's theorem. The main point is to show that parametricity isn't just for computer programs; physics looks like it is ripe with opportunities for applications of theorems for free.