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