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:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:A completeness proof for bisimulation in the pi-ca
lculus using Isabelle - Jesper Bengtson\, Uppsala
University
DTSTART;TZID=Europe/London:20080117T140000
DTEND;TZID=Europe/London:20080117T150000
UID:TALK10240AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/10240
DESCRIPTION:We use the interactive theorem prover Isabelle to
prove that\nthe algebraic axiomatization of bisimu
lation equivalence in the pi-calculus is sound and
complete. This is the ﬁrst proof of its kind to b
e wholly machine checked. Although the result has
been known for some time the proof had parts which
needed careful attention to detail to become comp
letely formal. It is not that the result was ever
in doubt\; rather\, our contribution lies in the m
ethodology to prove completeness and get absolute
certainty that the proof is correct\, while at the
same time following the intuitive lines of reason
ing of the original proof. Completeness of axiomat
izations is relevant for many variants of the calc
ulus\, so our method has applications beyond this
single result. We build on our previous eﬀort of i
mplementing a framework for the pi-calculus in Isa
belle using the nominal data type package\, and st
rengthen our claim that this framework is well sui
ted to represent the theory of the pi-calculus\, e
specially in the smooth treatment of bound names.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Sam Staton
END:VEVENT
END:VCALENDAR