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

## Recent comments

10 min 26 sec ago

1 hour 49 min ago

21 hours 3 min ago

21 hours 31 min ago

23 hours 34 min ago

1 day 3 hours ago

1 day 10 hours ago

1 day 11 hours ago

1 day 23 hours ago

1 day 23 hours ago