University of Cambridge > > Semantics Lunch (Computer Laboratory) > The Power of Parameterization in Coinductive Proof

The Power of Parameterization in Coinductive Proof

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Peter Sewell.

This will be the first Semantics Lunch of the term - please do come along (or email with offers of talks.

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

I will compare our theorem with the Knaster-Tarski theorem and show its power using a simple bisimulation example.

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

You can find the Coq library at

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

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity