For the journal version of the callcc paper, I propose the following outline:

1. Introduction.

   Essentially as now.

2. Adding callcc to ML.

   Essentially as now, with discussion of trade-off's.

3. Simple Types.

   Structured operational semantics, but using evaluation contexts rather
   than an ad-hoc language of continuations.

   Proof of soundness of typing with respect to this semantics.

   I will have to check into adapting the "observational soundness" stuff
   to the operational setting.

4. Polymorphism (Damas-Milner style)

   Discuss issues of soundness of pure D-M with respect to the
   continuation-passing operational semantics.  (cf Robin's remark)

   Show unsoundness of full D-M with callcc.  (Harper-Lillibridge ctx).
   Discuss intuition behind failure of soundness.  (cbv vs cbn let)

   Introduce a particular, restrictive type system that is sound, and prove
   the soundness theorem for it.

   Discuss alternatives (weak polymorphism, effects inference).

5. Conclusion.

   Soundness of simply-typed case may be established via cps transform,
   via a simple extension of Meyer-Wand.

   Interestingly, the cps transform doesn't appear to extend to D-M, even
   in the absence of continuation primitives.  This may be related to the
   difficulties encountered by Milner in proving soundness of pure ML with
   respect to a continuation-passing denotational semantics.

   Pointers to Felleisen and Wright's work, Gifford.


The main change is that I am dropping mention of cps conversion (other than in
the conclusion), and am replacing the use of denotational semantics by a new
form of operational semantics mid-way between Felleisen's system and the one I
introduced in the POPL paper.  (The main purpose of using denotational
semantics was that there is an obvious connection between the continuation
semantics of a term and the direct semantics of its cps conversion.)

Comments?
