Introduction to Deep Inference and New Ideas on Normalisation

Speaker(s): Alessio Guglielmi
Organiser:
Time: 23/05/2007 13:00-14:00
Location: B59/1257

Abstract

Deep inference is a relatively recent and ambitious development, aiming at refounding proof theory on more closely related grounds to computation than before. Normalisation is, of course, an integral part of the deep inference theory. In this talk, after having introduced deep inference, we will explore the new idea of `atomic flow'.

Atomic flows are diagrams, associated to proofs, that seem to capture essential aspects of normalisation, in a very abstract and yet very simple model. Their use allows us to control normalisation with unprecedented ease, and to generalise to a great extent existing normalisation theorems.

This is joint work with Tom Gundersen.