a first attempt at a type theory of delimited continuations

DelCont.txt

The main judgment of this system is the hypothetical judgment

    Γ ; K ; S ⊢ M : A true

where @Γ@ is a standard type context, @K@ is a set of in-scope reset points
for the delimited continuations, and @S@ is an optional in-scope shift
indicating what the most recent shift term needs for it's hole type. @K@ and
@S@ are defined as

    K ::= e | K, k : A resets B
    S ::= e | s : A shifts B

These are used in the following judgmental fragment:


    Γ ; K, k : A resets B ; S ⊢ M : B true
    --------------------------------------
     Γ ; K ; S ⊢ reset[k;A;B](M) : B true
    
    
             e ; K ; s : A shifts B ⊢ M : B true
    ------------------------------------------------------
    Γ ; K, k : A resets B ; S ⊢ shift[k;s;A;B](M) : A true
    
    
                Γ ; K ; e ⊢ M : A true
    ------------------------------------------------
    Γ ; K ; s : A shifts B ⊢ continue[s](M) : B true


We can internalize certain aspects of these judgments as follows:


           Γ ; K ; e ⊢ M : A true
    ------------------------------------
    Γ ; K' ; S' ⊢ wrap[K](M) : [K]A true
    
    
    Γ ; K ; S ⊢ M : [K']A true    K' ⊆ K
    ------------------------------------
       Γ ; K ; S ⊢ unwrap(M) : A true


The type @[K]A@ represents @A@'s that need to reset to positions @K@. For
example, the term @shift[k;s;A;B](foo(continue[k](bar)))@ is an @A@ whenever
there is a reset point @k : A resets B@ in scope, but by itself is not an @S@,
so we can wrap it up as
@wrap[k : A resets B](shift[k;s;A;B(foo(continue[k](bar)))])@ which has
the type @[k : A resets B]A@.

Conversely, we can unwrap such terms precisely when the reset scope has the
resets we need to correctly run the continuation.

The connective has the obvious, boring computation rule
@unwrap(wrap[K](M)) => M@. All the interesting computation here is in the
purely judgmental fragment. We'll use a meta-function @RESET@ that will be
helpful. Omitting types in terms:


    Γ ; K, k : A resets B ; S ⊢ M : B
    ---------------------------------  =>  Γ ; K ; S ⊢ RESET(k,M) : B true
    Γ ; K ; S ⊢ reset[k](M) : B true
    
    
Where @RESET@ is defined as


    RESET(k, M) = M
      when k is not used in M
    RESET(k, M{ shift[k;s](K{ continue[s](N) }) }) = RESET(k, K{M{N}})
      when M{ } has no resets nor shift's around it's hole


This definition of @RESET@ is ok because the rules for @shift@ and @reset@
work in conjunction to make @K@ a stack, where @reset@ pushes a name to the
stack, and @shift@ pops one, so that access to reset points is always reverse
of the order in which they were introduced. If @M{ }@ has a reset around the
hole, that must be computed first. If @M{ }@ has a shift to @k@ around its
hole, the higher shift must reset first.

@psygnisfive This looks plausible/interesting. Why not try formalizing it in Twelf to see if it holds water?