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.
