Lambda the Ultimate

BCS FACS - Annual Peter Landin Semantics Seminar: Rationalism v Hardware
Date/Time: Monday 2 December 2013, 6.00pm - 8.30pm

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

Cost to attend: Free of charge, but, please book your place via the BCS online booking system.

Book Online: https://events.bcs.org/book/832/

Synopsis:

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 "Rationalism versus hardware" and will be delivered by Professor Richard Bornat (Middlesex University).

Programme

5.15pm

Coffee

6.00pm

Welcome & Introduction

6.05pm

Peter Landin Semantics Seminar

Rationalism v Hardware - Professor Richard Bornat (Middlesex University)
7.20pm

Drinks Reception

Seminar details

Peter Landin's great contribution was to show that programming could be abstracted from hardware and made the subject of mathematical study. That work was fundamentally rationalist: his thesis was that unless programming fits the lambda calculus, we could never understand it. But empiricism cannot be defeated, and hardware inevitably pricked rationalist complacency with fixed size integers, array overflow, null dereference and lots, lots more.

Now the primacy of the rationalist approach has been challenged afresh with the rise of multiprocessors. In the pursuit of speed, execution is no longer sequential and memory is no longer simply shared. A multicore processor is a distributed system, and different designers make different arbitrary choices in an attempt to make their systems programmable. The risks are obvious, and the remedy isn't clear.

Rationalists are fighting back, and we already have rational models of hardware that cover the range of modern processors. But we are far from winning, and the attempt to define C and C++ as hardware-independent concurrent languages seems to be flawed.

This talk will survey the state of the battle - trying not to frighten you too much - and will include a presentation of my own attempt to produce a program logic for multiprocessor concurrency (joint work with Jade Alglave, Peter O'Hearn and Matthew Parkinson). Although Peter Landin didn't approve of program logic, I hope he would have approved our attempts to lift programming once again above the level of what he always called `instrumentation'.