Programme

14.00 - 15.00:

Proof Theory, Semantics, and Operating Systems
Peter O'Hearn, Queen Mary, University of London

I will describe how some seemingly abtruse concepts in the semantics of programming languages correspond directly to intuitive design principles underpinning the operating systems that power the computers we all use every day. Proof theory is then the conduit, through which these concepts can flow into practical tools for analyzing low-level systems programs. For good measure, I will also draw in some concepts from artificial intelligence and philosophy of science along the way.

15.00 - 15.30:

Coffee

15.30 - 16.15:

Shedding Light on Obscure Terms in Rewriting
Fer-Jan de Vries, University of Leicester

Confluence is a property we all love. The move from finite to infinite rewriting systems can lead to loss of confluence. We will demonstrate this by examples. The unique normal form property has a better chance of surviving such a move. To regain confluence and UN in the infinitary setting one has to identify the "obscure" terms. We will give a new axiomatisation of such terms. Choosing a set of obscure terms for a rewrite system is a kin to choosing a semantics.

16.15 - 17.00:

The Construction of Infinity
Venanzio Capretta, University of Nottingham

The status of infinity has been a philosophical battleground since Antiquity. Greek philosophers already debated whether it can be conceived as existing in actuality or just as potential unboundedness. The treatment of actual infinite objects has been seen across history as a province of metaphysics or as a technical trick to solve some mathematical problems. Starting with Cantor, infinite sets of different sizes have been given a precise mathematical status, leading eventually to modern set theory. However, fierce criticism was fired at this conception by constructivist and predicativist thinkers.

In recent decades, significant advances have been made in the constructive understanding of infinity. At first it may seem that computer science should be impervious to any notion of infinite object: computers are discrete machines with a finite memory. Surprisingly, mathematical methods to represent infinite objects and compute with them have been devised. It even turns out that some computational problems are best solved by using infinite data structures.

I will give a brief historical review of the computational treatment of infinity and explain the basic mathematical notions that are being developed in this field.

Afterwards we will retire to a local pub and then on to dinner for anyone who would like to join us.

Travel

Lecture Theatre A25
Business School South Building
Jubilee Campus, University of Nottingham
Wollaton Road, Nottingham NG8 1BB

Travel information and a map of the Jubilee Campus are available here. The seminars will be held in room A25 of the Business School South Building (labelled 7 on the campus map).

By train or bus: The Jubilee Campus is around 10 minutes by taxi from the train and bus stations in Nottingham city centre. Online timetables and booking are available for both trains and buses.

By car: The University of Nottingham has a policy of discouraging the use of cars and encouraging alternative modes of transport. But if you need to travel by car, please enter the campus itself via the main entrance on Wollaton Road, as the other entrance (on Triumph Road) is only accessible with an electronic pass. Tell the security staff at the main entrance that you are a visitor, and they will direct you to the pay-and-display visitors car park nearby. Make sure not to park elsewhere, as all other spaces require a parking permit and are subject to clamping.

In case you require a taxi as part of your return journey, here are some local numbers:

Cable Cars:	0115 922 9229
Central Taxi:	0115 975 2222
County Taxi:	0115 942 5425
DG Taxi:	0115 960 7607

Contact