BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Power of Parameterization in Coinductive Proof - Chung-Kil Hur
 \, MSR
DTSTART:20121022T120000Z
DTEND:20121022T130000Z
UID:TALK41152@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:In this talk\, I will present a very simple theorem about coin
 duction\, which we call parameterized coinduction. More precisely it is fo
 r reasoning about the greatest fixed point of a monotone function on a com
 plete lattice. The theorem is as simple as the Knaster-Tarski fixedpoint t
 heorem but gives a more powerful reasoning\nprinciple.\n\nI will compare o
 ur theorem with the Knaster-Tarski theorem and show its power using a simp
 le bisimulation example.\n\nIn a different point of view\, the theorem cap
 tures a semantic notion of "guarded proof" in coinduction. Thus we impleme
 nted a new tactic "pcofix" replacing Coq's primitive cofix and avoiding it
 s syntactic guardedness checking of proof terms.\n\nYou can find the Coq l
 ibrary at\n\nhttp://plv.mpi-sws.org/paco\n\nThis is joint work with Georg 
 Neis\, Derek Dreyer and Viktor Vafeiadis.\n
LOCATION:FW26
END:VEVENT
END:VCALENDAR