# 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

### Towards Generating Compact Proof Certificates for Observational Equivalence

- Date
- Tuesday, December 04 2012 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Alwen Tiu (Australian National University, Canberra)

Observational equivalence, in the context of process calculi, is a
notion of behavioral equivalence defined via observable actions of
processes. It is commonly defined co-inductively using the transitions
of the processes, and, more importantly, it needs to be closed under
arbitrary process contexts. Due to the latter requirement, it is
difficult to mechanise observational equivalence checking directly,
and various methods for approximating observational equivalence have
been proposed in the literature. In this talk I will consider an
approximation of observational equivalence, for the spi-calculus,
based on labelled bisimulation, and present a procedure for checking
this notion of bisimulation. This procedure has been implemented in a
logical framework called Bedwyr. As the procedure and its
implementation are quite complex, to increase confidence in the result
of the implemention, the prover (called SPEC) needs to produce an
explicit proof object, in terms of a bisimulation set, that can be
checked independently outside the prover. Initial experiments suggest
that often such a set can be very large, even for simple processes. I
will discuss several simplifications to reduce the size of the
bisimulation set that are currently implemented in SPEC, exploiting
the so-called 'bisimulation-up-to' techniques, originally developed by
Milner, Sangiorgi and others for the pi-calculus. I will then discuss
some directions for future work, in particular incorporating more
general up-to techniques as logical theories in a logical framework.