BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Isaac Newton Institute Seminar Series
SUMMARY:Experiments with Concurrent Kleene Algebra - Bernh
ard MÃ¶ller (UniversitÃ¤t Augsburg)
DTSTART;TZID=Europe/London:20220705T093000
DTEND;TZID=Europe/London:20220705T103000
UID:TALK175733AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/175733
DESCRIPTION:This talk is on the foundational side. In 2009\, C
oncurrent Kleene Algebra (briefly CKA) was defined
as an extension of Kleene Algebra\, adding to seq
uential composition several variants of concurrent
composition while preserving the standard laws. T
he aim was to allow\, in parallel to operational o
r assertion-logical deduction\, also algebraic\, (
in)equational proofs about concurrent systems. Thi
s is particularly interesting\, since (in)equation
al reasoning is very suitable for semi-automatic o
r even automatic proofs. CKA has met considerable
interest. We discuss some new twists about it.\n-
We present a new definition technique for partial
operators\, namely an assume/claim style akin to t
he rely/guarantee format of program specification.
This admits a general way of defining a refinemen
t relation as well as Top and Bottom elements of t
he refinement order.\n- We experiment with the gra
ph model of the algebra\, in particular how state-
like entities could be defined\, along with image
and inverse image operators. This allows a form of
Hoare triples and relates to O'Hearn's resource v
iew of these. It remains to be seen whether a pure
ly algebraic abstraction of the approach can be fo
und.\nThe talk is based on unpublished joint work
with Tony Hoare.\n \;
LOCATION:Seminar Room 1\, Newton Institute
CONTACT:
END:VEVENT
END:VCALENDAR