Séminaire,
March 14, 2013

## Chung-Kil Hur (Microsoft Research Cambridge), The Power of Parameterization in Coinductive Proof

### Schedule

- March 14, 2013, 14:00 - 15:00

### Abstract

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

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