BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Lecture 3: Logic for Program Development\, Verification and Implem
 entation. - Tony Hoare\, FRS FREng
DTSTART:20180504T130000Z
DTEND:20180504T140000Z
UID:TALK99919@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:Tony Hoare\, FRS FR Eng\, Hon Mem Cambridge University Computi
 ng Laboratory.\n\nWe start with a sufficient resume of previous lectures\,
  so prior attendance at the lectures on Geometry and Algebra is not a requ
 irement. Interested researchers may consult the lecture notes on my person
 al page of the Departmental Website. \n \nWe then derive from the algebra 
 a set of logical rules of reasoning about concurrent programs. The derivat
 ion can be reversed: from the Rules to the Algebra.\n \nWe then give algeb
 raic definitions of Milner/Plotkin transitions\, and of Hoare/O’Hearn Tr
 iples\, and by simple translation obtain the traditional rule of Operation
 al Semantics and Verification Logic.  They are simply duals of each other.
LOCATION:FW26
END:VEVENT
END:VCALENDAR