Résumé de séminaire

Résumé :

Closed reduction strategies in the lambda-calculus restrict the reduction rules: the idea is that reductions can only take place when certain terms are closed (i.e. do not contain free variables). This has lead to various applications, such as an alpha-conversion free calculus of explicit substitutions, and an efficient abstract machine. In this talk I will describe a new application of this strategy to a linear version of Goedel's System T. We will show that a linear System T with closed reduction offers a huge increase in expressive power over the usual linear systems, which are `closed by construction' rather than `closed at reduction'.

This is joint work with Sandra Alves, Mario Florido and Ian Mackie, partially funded by the Treaty of Windsor Grant: "Linearity: Programming Languages and Implementations"