Ian Mackie - Closed Reductions in the Lambda-calculus
Closed reductions in the lambda-calculus is a strategy for a calculus of explicit substitutions which overcomes many of the usual syntactical problems of substitution. This is achieved by only moving closed substitutions through certain constructs. As a consequence we obtain a weak calculus, but nevertheless it is rich enough to capture the usual strategies in the lambda-calculus (call-by-value, call-by-need, etc.) and is adequate for the evaluation of programs. An interesting point is that the calculus permits substitutions to move through abstractions, and reductions are allowed under abstractions, if certain conditions hold. As a consequence, the calculus naturally provides an efficient notion of reduction (with sharing), which can easily be implemented.
This is joint work with Maribel Fernandez.