CWS paper

[Matthew Fluet]

> I'm a bit confused by your analysis.  Here's what I understand after the latest
> modification.
> 
> RCont = Func U Jump U {bot}
> REnv = Func -> RCont

I think it will be 

REnv = (Func U Jump) -> RCont

because you want the rule:

R[let fun k <xi>* = e in e']p = R[e]p' V Gamma
 where Gamma = R[e']p and p' = Gamma(k)

> Here is your latest definition of <=l, which is a reflexive, transitive binary
> relation on RCont.
> 
> > bot <=l l' <=l l   forall l' in Label
> 
> I'm afraid I don't understand what this means.  Where is "l" quantified?  As
> best as I can make out, this says that every label is <=l every other label.
> I.E. the relation is pretty trivial.
> 
> Can you define <=l again for me?
> 
> Do you mean for <=l to be a partial order?

I want <=l to the partial order imposed on RCont when interpreted relative
to the label l.  The partial order on REnv is "pointwise" in the sense
that it's defined as:

Gamma1 <= Gamma2
iff
forall l in Label. Gamma1(l) <=l Gamma2(l)
                   where
                   bot <=l l' <=l l   forall l' in Label

So, (Func U Jump U {bot}, <=l) corresponds to the squashed powerset
domain, with bot for {}, l' for {l'} (where l' <> l), and l for everything
else.