BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Semantics Lunch (Computer Laboratory)
SUMMARY:The Power of Parameterization in Coinductive Proof
- Chung-Kil Hur\, MSR
DTSTART;TZID=Europe/London:20121022T130000
DTEND;TZID=Europe/London:20121022T140000
UID:TALK41152AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/41152
DESCRIPTION:In this talk\, I will present a very simple theore
m about coinduction\, which we call parameterized
coinduction. More precisely it is for reasoning ab
out the greatest fixed point of a monotone functio
n on a complete lattice. The theorem is as simple
as the Knaster-Tarski fixedpoint theorem but gives
a more powerful reasoning\nprinciple.\n\nI will c
ompare our theorem with the Knaster-Tarski theorem
and show its power using a simple bisimulation ex
ample.\n\nIn a different point of view\, the theor
em captures a semantic notion of "guarded proof" i
n coinduction. Thus we implemented a new tactic "p
cofix" replacing Coq's primitive cofix and avoidin
g its syntactic guardedness checking of proof term
s.\n\nYou can find the Coq library at\n\nhttp://pl
v.mpi-sws.org/paco\n\nThis is joint work with Geor
g Neis\, Derek Dreyer and Viktor Vafeiadis.\n
LOCATION:FW26
CONTACT:Peter Sewell
END:VEVENT
END:VCALENDAR