COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > A completeness proof for bisimulation in the pi-calculus using Isabelle

## A completeness proof for bisimulation in the pi-calculus using IsabelleAdd to your list(s) Download to your calendar using vCal - Jesper Bengtson, Uppsala University
- Thursday 17 January 2008, 14:00-15:00
- Room FW11, Computer Laboratory, William Gates Building.
If you have a question about this talk, please contact Sam Staton. Note the unusual day. We use the interactive theorem prover Isabelle to prove that the algebraic axiomatization of bisimulation equivalence in the pi-calculus is sound and complete. This is the ﬁrst proof of its kind to be wholly machine checked. Although the result has been known for some time the proof had parts which needed careful attention to detail to become completely formal. It is not that the result was ever in doubt; rather, our contribution lies in the methodology to prove completeness and get absolute certainty that the proof is correct, while at the same time following the intuitive lines of reasoning of the original proof. Completeness of axiomatizations is relevant for many variants of the calculus, so our method has applications beyond this single result. We build on our previous eﬀort of implementing a framework for the pi-calculus in Isabelle using the nominal data type package, and strengthen our claim that this framework is well suited to represent the theory of the pi-calculus, especially in the smooth treatment of bound names. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Computer Laboratory talks
- Computing and Mathematics
- Logic and Semantics Seminar (Computer Laboratory)
- Room FW11, Computer Laboratory, William Gates Building
- School of Technology
Note that ex-directory lists are not shown. |
## Other listsThe obesity epidemic: Discussing the global health crisis Sainsbury Laboratory Seminars "See Naples and Dial - An italian Job"## Other talksThe Global Warming Sceptic My Life in Science Seminar Planck Stars: theory and observations Rather more than Thirty-Nine Steps: the life of John Buchan Access to Medicines Computing knot Floer homology mTORC1 signaling coordinates different POMC neurons subpopulations to regulate feeding TBC An approach to the four colour theorem via Donaldson- Floer theory Inferring the Evolutionary History of Cancers: Statistical Methods and Applications Doctor Who: Gridlock |