Linearly-used Continuations and Self-duality

Add to your list(s) Download to your calendar using vCal

• Alex Simpson, University of Edinburgh
• Thursday 17 December 2009, 14:00-15:00
• UG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

Berdine et al (HOSC 2002) demonstrated that, in many structured forms of control, continuations are used in a linear fashion. Based on this, Hasegawa (FLOPS 2002, FLOPS 2004 ) recast the standard call-by-value and call-by-name continuation-passing-style (CPS) transformations using linear types to reflect linear usage. In this talk I shall examine Hasegawa’s linearly-used CPS translations from a fresh viewpoint. I shall argue that the natural target language for the translations is a generalisation of intuitionistic linear logic, the “enriched effect calculus”, obtained by adding certain constructs from linear logic to Moggi’s computational metalanguage. The enriched effect calculus is weak enough that it conservatively extends Moggi’s metalanguage. Nevertheless, it is rich enough to express several applications of linear logic, including linearly-used continuations.

In the enriched effect calculus, Hasegawa’s call-by-name and call-by-value linearly-used CPS translations are subsumed by a single generic CPS translation of the enriched effect calculus into itself. This generic translation enjoys a remarkable property, unexpected of CPS translations: it is involutive. That is, the translation of the translation of a term is equal to the original term (modulo type isomorphism). This property constitutes the main syntactic theorem of the talk. As a corollary, we obtain full completeness results for the call-by-name and call-by-value linearly-used CPS translations into the enriched effect calculus.

The main syntactic theorem is proved using a category-theoretic semantics for the enriched effect calculus, which illuminates a fundamental aspect of linearly-used continuations. From any model of the enriched effect calculus one can construct an associated linearly-used CPS model. In a natural sense, the constructed model is dual to the original model. In particular, every model is isomorphic to its own double dual; hence, surprisingly, every model of the enriched effect calculus arises as a linearly-used CPS model with respect to another model (its dual model). Moreover, the syntactic linearly-used CPS translation of the enriched effect calculus into itself is derived semantically as the canonical morphism from the syntactic (initial) model to its dual. This morphism is, in fact, an equivalence of models, and thus the synactic model is self dual. The main syntactic theorem is a consequence of this self duality.

This is joint work with Jeff Egger and Rasmus Mogelberg.

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
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.