Lambda the Ultimate

Peter Landin Annual Semantics Seminar

6 December 2010

BCS London Offices

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

http://www.bcs.org/upload/pdf/london-office-guide.pdf

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 the area of semantics will pay tribute
to Landin's contribution to computing through a public seminar. The first
such seminar will be delivered by Professor John Reynolds (Queen Mary,
University of London, Imperial College and Carnegie Mellon University).
Professor Cliff Jones (Newcastle University) will introduce and chair
the seminar.

Immediately before the seminar, a rare film of a lecture Peter Landin gave at
the Science Museum in 2001 will be replayed.

Programme
-----------------

5pm Coffee
5:25pm Welcome and Introduction (Prof. Cliff Jones)
5.35pm Film of Peter Landin talk at the Science Museum, 2001
5.55pm Introduction to seminar
6pm Peter Landin Semantics Seminar:

Toward a Grainless Semantics for Shared-Variable Concurrency
(Prof. John Reynolds)

7.15pm Close (Prof. Cliff Jones)
7.20pm - 8.20pm Drinks Reception

Registration
-----------------

If you would like to attend, please email Paul.Boca@googlemail.com by
3 December.

Seminar details
-----------------------

TOWARD A GRAINLESS SEMANTICS FOR SHARED-VARIABLE CONCURRENCY

Prof. John C. Reynolds
Queen Mary, University of London
Imperial College
Carnegie Mellon University

Conventional semantics for shared-variable concurrency suffers from the
"grain of time" problem, i.e., the necessity of specifying a default
level of atomicity. We propose a semantics that avoids such a choice
by regarding all interference that is not controlled by explicit
synchronization as catastrophic. It is based on three principles:

- Operations have duration and can overlap one another
during execution.

- If two overlapping operations touch the same location, the
meaning of the program execution is ``wrong''.

- If, from a given starting state, execution of a program can
give "wrong", then no other possibilities need be considered.

In our current approach, instead of trace sets, we use trace trees, in
which we separate nondeterminism and branching.