Lambda the Ultimate

(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.Boca@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.

Given,

f : ∀a:*. a → a → a

we can take a = {x,y} to show that for a particular x,y, either:

f x y = x, or 
f x y = y

My question is how to formally reason that f is uniformly defined by one of those equations. What property of f is needed? Informally, it's easy to reason that there is nothing f could branch on, but I don't see how to generalize.

Thanks