Lambda the Ultimate

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
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.