The language X: term rewriting, continuations and classical types, and the impossibility of filter semantics

Add to your list(s) Download to your calendar using vCal

• Steffen van Bakel, Imperial College London
• Friday 25 November 2011, 16:00-17:00
• LG52 Learning Centre.

If you have a question about this talk, please contact Paul Levy.

We will present the language X that describes a calculus of connections that has been designed to give a Curry-Howard correspondence to Gentzen’s sequent calculus for implicative classical logic.

The symmetry of the cut-elimination procedure for proofs is reflected by a symmetry in the reduction relation on X. To demonstrate the expressive power of X, we will show how, even in an untyped setting, more and more elaborate calculi can be embedded into X. We describe how the symmetrical reductions of X account for the call-by-name and call-by-value evaluations.

We will show how ‘normal’ calculi like the lambda calculus, lambda-mu and Curien-Herbelin’s calculus can be safely embedded in X.

We will finish by defining what should be the natural intersection-union type system for X, but argue that it (surprisingly) does not generate filter semantics.

The talk is a summary of work performed over the last nine years, in part in collaboration with Stephane Lengrand and Pierre Lescanne.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG52 Learning Centre
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.