Monday, February 22, Volen 101, 3-5 p.m.
(This meeting continues a fortnightly research seminar at Brandeis on programming language theory and implementation. It is being run jointly with the Church group at Boston University---on alternate weeks we meet at BU.)
In a previous seminar, we considered the problem of constructing an optimal implementation of the lambda calculus. One solution involves encoding a lambda term as a proof net, according to any embedding of intuitionistic logic into linear logic. The proof net can be reduced incrementally, using only local reduction rules. This strategy performs the minimum number of beta steps, as defined by Lvy. In this talk, we show how to extend this technology to a language with control operators.
The essential problem in implementing optimal reduction of a language with control operators is to encode continuations such that they can be duplicated incrementally, without destroying optimality. Our solution is derived from a surprisingly simple transformation on graphs of continuation-passing style terms.
As an application of this technique, we show how to achieve optimal reduction of the lambda calculus extended with Scheme's call/cc operator. The result is an implementation of call/cc that is independent of evaluation order. Furthermore, our approach provides a simpler account of a previous implementation of call/cc using proofnets. We can apply the same approach to any control operator that can be encoded in the pure lambda calculus using a continuation-passing style translation. In particular, we have investigated Parigot's lambda-mu calculus and Filinski's symmetric lambda calculus.