![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Monday 22 October 2012, 13:00-14:00
The Power of Parameterization in Coinductive Proof
- đ¤ Speaker: Chung-Kil Hur, MSR
- đ Date & Time: Monday 22 October 2012, 13:00 - 14:00
- đ Venue: FW26
Abstract
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.
Series This talk is part of the Semantics Lunch (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Department of Computer Science and Technology talks and seminars
- FW26
- Interested Talks
- Martin's interesting talks
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.