BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A completeness proof for bisimulation in the pi-calculus using Isa
 belle - Jesper Bengtson\, Uppsala University
DTSTART:20080117T140000Z
DTEND:20080117T150000Z
UID:TALK10240@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:We use the interactive theorem prover Isabelle to prove that\n
 the algebraic axiomatization of bisimulation equivalence in the pi-calculu
 s is sound and complete. This is the first proof of its kind to be wholly
  machine checked. Although the result has been known for some time the pro
 of had parts which needed careful attention to detail to become completely
  formal. It is not that the result was ever in doubt\; rather\, our contri
 bution lies in the methodology to prove completeness and get absolute cert
 ainty that the proof is correct\, while at the same time following the int
 uitive lines of reasoning of the original proof. Completeness of axiomatiz
 ations is relevant for many variants of the calculus\, so our method has a
 pplications beyond this single result. We build on our previous effort of
  implementing a framework for the pi-calculus in Isabelle using the nomina
 l data type package\, and strengthen our claim that this framework is well
  suited to represent the theory of the pi-calculus\, especially in the smo
 oth treatment of bound names.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR