University of Cambridge > Talks.cam > 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 Peter.Sewell@cl.cam.ac.uk) 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

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

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-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity