BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A structural proof of the soundness of rely/guarantee rules - Clif
 f Jones\, Newcastle University
DTSTART:20061027T130000Z
DTEND:20061027T140000Z
UID:TALK5612@talks.cam.ac.uk
CONTACT:Tom Ridge
DESCRIPTION:The challenge of finding compositional ways of (formally) deve
 loping concurrent programs is considerable. Various forms of rely and guar
 antee conditions have been used to record and reason about interference in
  ways which do indeed provide compositional development methods for such p
 rograms. This paper presents a new approach to justifying the soundness of
  rely/guarantee inference rules. The underlying concurrent language is def
 ined by an operational semantics which allows fine-grained interleaving an
 d nested concurrency\; the proof that the rely/guarantee rules are consist
 ent with that semantics (including termination) is by a structural inducti
 on.\n\nA lemma which relates the states which can arise from the extra int
 erference that results from taking a portion of the program out of context
  is key to our ability to do the proof without having to perform induction
  over the computation history. This lemma also offers a way to understand 
 some elusive expressibility issues around rely guarantee conditions.\n
LOCATION:FW11
END:VEVENT
END:VCALENDAR