Lambda the Ultimate

Coinductive proof principles for stochastic processes, Dexter Kozen, Logical Methods in Computer Science 2007.

We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique. The rule encapsulates low-level analytic arguments, allowing reasoning about such processes at a higher algebraic level. We illustrate the use of the rule in deriving properties of a simple coin-flip process.

This paper has a clever little program, a clever little proof principle for it, and exploits connections to a bit of mathematics you don't normally see in PL research.