The Power of Parameterization in Coinductive Proof

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

• Chung-Kil Hur, MSR
• Monday 22 October 2012, 13:00-14:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory talks
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.