In this talk, I will present a very simple principle for reasoning about coinduction, which we call parameterized coinduction. More precisely, it is a theorem about the greatest fixed point of a monotone function on a complete lattice. This theorem is as simple as the Tarski's fixed-point theorem but provides a more useful reasoning principle.

In a different point of view, the principle captures a semantic notion of "guarded proof" in coinduction. Thus we implemented a new tactic "pcofix" replacing Coq's primitive tactic "cofix" and avoiding its syntactic guardedness checking of proof terms.

You can find the Coq library 'Paco' that provides the tactic 'pcofix' at

http://plv.mpi-sws.org/paco

This is joint work with Georg Neis, Derek Dreyer and Viktor Vafeiadis.