We still have some places left if you would like to join us for the
Peter Landin seminar, which this year will be given by Prof. Cliff
Jones.

Please let me know as soon as possible if you would like to attend.

Best wishes

Paul Boca
______

(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  (Professor Edmund Robinson, QMUL)
6.05pm Peter Landin Semantics Seminar:

                "To be or not to be" valid?

        Professor Cliff Jones (University of Newcastle)

7.20pm Close (Prof Edmund Robinson)
7.25pm Presentation of BCS award (Dr Bill Mitchell, BCS)
7.30pm - 8.30pm Drinks Reception

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

If you would like to attend, please email Paul.B...@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.