School of Computer Science
University of Birmingham
2pm, Friday 21 February 2005
Room 2511, JCMB, King's Buildings
In this talk, we describe two cases where (impredicative) polymorphism is useful for analyzing Continuation Passing Style (CPS) by enabling parametricity reasoning. The first case involves a call-by-value language with the control operator call/cc and a type-and-effect system for control effects, while the second is about relating the two call-by-name CPS transforms from the literature.
Type-and-effect systems refine type systems by capturing where effects may occur, and more importantly, how far they can propagate. For control, the effects say roughly whether an expression may result in jumping, and if so how far. We CPS-transform a simple type-and-effect system to a target language with polymorphic types. In particular, this gives an analysis of effect masking.
There are two call-by-name CPS transforms, one published by Plotkin in 1975, and a much more recent one due to Thomas Streicher. They appear quite different; one introduces fewer, the other more negations than the call-by-value CPS transform. We show that the Plotkin transform can be given a polymorphic typing with locally quantified answer types, and that with this restricted typing it becomes isomorphic to the Streicher transform. The isomorphism is constructed essentially the same as for the encoding of pairs in System F.
The talk is based on two papers that appeared in POPL'03 and ESOP'04.