Coinductive proof principles for stochastic processes

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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

[admin] Slight typo on link

Should be coinduction.pdf, not coinduction.bpdf.

The working link...

... is here.