BCS FACS Annual Peter Landin Semantics seminar

Monday 3 December 2012, 6.00pm - 8.30pm
(refreshments will be served from 5.15pm)

BCS, First Floor, The Davidson Building, 5 Southampton Street, London, WC2E 7HA | Map

Cost to Attend:
Free of charge

Unifying Theories of Programming

Professor Sir Tony Hoare (Microsoft Research)

Two Classical Theories of programming are (1) the Hoare calculus of triples, for proving correctness of sequential programs, and (2) the Milner calculus of transitions, for specifying the intended execution of concurrent processes. I have long thought of these theories as rivals. But I now realise that the axioms of both these theories can be defined and proved in terms of the elementary laws of programming. A new axiom called ‘exchange’ is provable from Milner's definition of concurrency, and also justifies the newer rules for concurrency that have been introduced in the Hoare Theory by separation logic.

View the presentation slides (PDF)