The Power of Closed Reduction

Closed reduction strategies in the lambda-calculus restrict the reduction rules: the idea is that reductions may 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'.