Annual Peter Landin Seminar: 6 December 2011, 6pm, Convent Garden -- speaker Prof. Cliff Jones

[paul...@googlemail.com]

(Apologies if you receive multiple copies of this announcement)

Peter Landin Annual Semantics Seminar


6 December 2011


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 computer science will pay tribute to
Landin's
contribution to computing through a public seminar. This year's
seminar is
entitled "To be or not to be" valid?, and will be given by Professor
Cliff Jones (University of Newcastle) -- see below for abstract


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

5.15pm Coffee
6 pm Welcome and Introduction
6.05pm Peter Landin Semantics Seminar:

"To be or not to be" valid?

Professor Cliff Jones (University of Newcastle)

7.20pm Close
7.20pm - 8.30pm Drinks Reception


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

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


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

"To be or not to be" valid?

Professor Cliff Jones (University of Newcastle)

Abstract:
The problem of reasoning about undefined terms has been "solved" (or
avoided) in a variety of ways. (Think about division by zero - but
undefinedness comes up in many ways in program specifications.) For a
long-time, I've used a non-standard logic (LPF) but few others have
joined this movement because such good tools exist for standard,
classical, logic. At some level, I believe that alternative approaches
are "workarounds". I'll try to show why the workarounds present
problems and report on recent positive ideas for mechanising LPF in a
way whose efficiency is close to that of classical logic. To make the
talk accessible to as wide an audience as possible, I'll place the
ideas in a framework that goes back (if not to Shakespeare, at least)
a long way.