University of Birmingham > Talks@bham > Theoretical computer science seminar > The language X: term rewriting, continuations and classical types, and the impossibility of filter semantics

## The language X: term rewriting, continuations and classical types, and the impossibility of filter semanticsAdd 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. |
## Other listsCondensed Matter Group Meetings Type the title of a new list here Particle Physics Seminars## Other talksUltrafast Spectroscopy and Microscopy as probes of Energy Materials TBA TBA The tragic destiny of Mileva MariÄ‡ Einstein Waveform modelling and the importance of multipole asymmetry in Gravitational Wave astronomy Quantum Sensing in Space |