LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
A formalization of bisimulation-up-to techniques and their meta-theory
- Date
- Tuesday, January 21 2014 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Matteo Cimini (LIX, Ecole Polytechnique)
Bisimilarity of two processes is formally established by producing a bisimulation relation, i.e. a set of pairs of process expressions that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and even infinite.
The bisimulation-up-to technique has been developed to reduce the size of the relations to exhibit while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques make defining candidate relations easier and they significantly reduce the amount of work in proofs. Furthermore, they are increasingly becoming a crucial ingredient in the automated checking of bisimilarity.
In this talk, we present our experience in using the Abella theorem prover for the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the pi-calculus. Our formalization is based on recent work on the proof theory of least and greatest fixpoints for accommodating the heavy use of coinductively defined relations and coinductive proofs about such relations. An important feature of our formalization is that our definitions and proofs are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. The presence of binders, as in the pi-calculus, is notoriously a delicate aspect to treat in formal proofs but we show that the underlying proof theoretic foundations of Abella makes it possible to smoothly lift the results from CCS to the pi-calculus. This is thanks to the use of lambda-tree syntax and generic reasoning through the nabla quantifier.