BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Experiments with Concurrent Kleene Algebra - Bernhard Möller (Uni
 versität Augsburg)
DTSTART:20220705T083000Z
DTEND:20220705T093000Z
UID:TALK175733@talks.cam.ac.uk
DESCRIPTION:This talk is on the foundational side. In 2009\, Concurrent Kl
 eene Algebra (briefly CKA) was defined as an extension of Kleene Algebra\,
  adding to sequential composition several variants of concurrent compositi
 on while preserving the standard laws. The aim was to allow\, in parallel 
 to operational or assertion-logical deduction\, also algebraic\, (in)equat
 ional proofs about concurrent systems. This is particularly interesting\, 
 since (in)equational reasoning is very suitable for semi-automatic or even
  automatic proofs. CKA has met considerable interest. We discuss some new 
 twists about it.\n- We present a new definition technique for partial oper
 ators\, namely an assume/claim style akin to the rely/guarantee format of 
 program specification. This admits a general way of defining a refinement 
 relation as well as Top and Bottom elements of the refinement order.\n- We
  experiment with the graph model of the algebra\, in particular how state-
 like entities could be defined\, along with image and inverse image operat
 ors. This allows a form of Hoare triples and relates to O'Hearn's resource
  view of these. It remains to be seen whether a purely algebraic abstracti
 on of the approach can be found.\nThe talk is based on unpublished joint w
 ork with Tony Hoare.\n&nbsp\;
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR