(Apologies if you receive multiple copies of this announcement)
****** still a few places left -- please register as soon as possible ********
Peter Landin Annual Semantics Seminar
3 December 2012
BCS London Offices
First Floor, The Davidson Building
5 Southampton Street
London
WC2E 7HA
http://www.bcs.org/upload/pdf/london-office-guide.pdf
https://events.bcs.org/book/361/
Introduction
----------------
Peter Landin (1930--2009) was a pioneer whose ideas underpin modern computing.
In the the 1950s and 1960s, Landin showed that programs could be
defined in terms of mathematical functions, translated into functional
expressions in the lambda calculus, and their meaning calculated with
an abstract mathematical machine. Compiler writers and designers of
modern-day programming languages alike owe much to Landin's pioneering
work.
Each year, a leading figure in computer science will pay tribute to
Landin's contribution to computing through a public seminar. This
year's seminar is entitled "Unifying Theories of programming" and
will be delivered by Professor Sir Tony Hoare (Microsoft Research).
Programme
-----------------
5.15pm Coffee
6 pm Welcome and Introduction (Professor Peter O'Hearn, UCL)
6.05pm Peter Landin Semantics Seminar:
Unifying Theories of programming
Professor Sir Tony Hoare (Microsoft Research)
7.20pm Close
7.20pm - 8.30pm Drinks Reception
Registration
-----------------
If you would like to attend, please register online:
https://events.bcs.org/book/361/
Seminar details
-----------------------
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.