One paper finished, two new ones submitted.
Conor and I have just submitted the final version of "Productive Coprogramming with Guarded Recursion" to the publishers. Looking forward to ICFP in Boston!
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.
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.