BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
A formalization of bisimulation-up-to techniques and their m
eta-theory
STATUS:CONFIRMED
ATTENDEE;CN="Matteo Cimini
":
MAILTO:no@spam.com
DESCRIPTION:
Bisimilarity of two processes is formally established by pro
ducing a bisimulation relation\, i.e. a set of pairs of proc
ess expressions that contains those two processes and obeys
certain closure properties. In many situations\, particularl
y when the underlying labeled transition system is unbounded
\, these bisimulation relations can be large and even infini
te. The bisimulation-up-to technique has been developed to r
educe the size of the relations to exhibit while retaining s
oundness\, that is\, the guarantee of the existence of a bis
imulation. Such techniques make defining candidate relations
easier and they significantly reduce the amount of work in
proofs. Furthermore\, they are increasingly becoming a cruci
al ingredient in the automated checking of bisimilarity. In
this talk\, we present our experience in using the Abella th
eorem prover for the formalization of the meta theory of sev
eral major bisimulation-up-to techniques for the process cal
culi CCS and the pi-calculus. Our formalization is based on
recent work on the proof theory of least and greatest fixpoi
nts for accommodating the heavy use of coinductively defined
relations and coinductive proofs about such relations. An i
mportant feature of our formalization is that our definition
s and proofs are\, in most cases\, straightforward translati
ons of published informal definitions\, and our proofs clari
fy several technical details of the informal descriptions. T
he presence of binders\, as in the pi-calculus\, is notoriou
sly a delicate aspect to treat in formal proofs but we show
that the underlying proof theoretic foundations of Abella ma
kes it possible to smoothly lift the results from CCS to the
pi-calculus. This is thanks to the use of lambda-tree synta
x and generic reasoning through the nabla quantifier.
DTSTART;TZID=Europe/Paris:20140121T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201401211
100
UID:LSVsemLSV.201401211100@lsv.ens-cachan.fr
LOCATION:Salle de ConfĂ©rence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR