Peter Landin Annual Semantics Seminar

Date/Time:
Monday 6 December 2010, 5.00pm - 9.00pm

Venue:
BCS, First Floor, The Davidson Building, 5 Southampton Street, London, WC2E 7HA | Maps

Details:

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:

5.00pm - 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
6.00pm - 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.