BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Abstract separation algebra - Tony Hoare (Microsoft Research)
DTSTART:20101004T114500Z
DTEND:20101004T130000Z
UID:TALK25927@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:I show how both Hoare triples and Plotkin triples can be repla
 ced by an\nabstract algebra\, in which all the primitives are pairs and si
 ngletons\,\ni.e.\, constants\, binary operators and binary predicates. The
  algebra deals\nseparately but equally simply with both sequential and con
 current composition\nof programs\; and many further program primitives and
  structuring operators\nlike choice and disjoint concurrency can be introd
 uced individually\, one\nat a time. The relevant proof rules for Hoare Tri
 ples\, and the relevant\nPlotkin triples for operational semantics\, are d
 erived simply and separately\nfor each binary operator.\n\nFamiliar algebr
 aic properties - associativity\, commutivity\, monotonicity\,\nidempotence
  are widely reused. The interactions between operators can be\ndescribed j
 ust two at a time by distributivity laws. These include mutual\ndistributi
 on\, a weak form of the exchange law of two-category theory. This\nleads t
 o an elementary presentation of separation logic and of Kleene algebra.\n\
 nThus we extend to the mathematics of programming the old saying about mar
 riage:\n'two's fun\, three's none'. Down with the triple!\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR