info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Annual Peter Landin Semantics Seminar: Rationalism v Hardware, Prof. Richard Bornat, 2 December 2013, 6pm, London
3 views
Skip to first unread message
paul...@googlemail.com
Sep 30, 2013, 6:57:00 PM9/30/13
to
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'.
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'.
0 new messages