[PRL] fresh variables in call/cc

[Dave Herman]

IIRC, a common way to specify call/cc operationally is by turning the 
captured continuation back into an ordinary expression:

     e ::= x | \x.e | (e e) | (call/cc e) | (abort e)
     v ::= \x.e
     E ::= [] | (E e) | (v E)

     E[\x.e v]    -> E[e[v/x]]
     E[call/cc v] -> E[v[\z.abort(E[z])]]  (z fresh w.r.t. E)
     E[abort e]   -> e

Is the freshness condition necessary for the call/cc rule? It looked 
"obvious" to me, since you don't want the variable representing the hole 
to be captured, but I can't see *how* it could be captured. AFAICT, you 
can't put the hole under a binder in this language, and rightly so; we 
don't evaluate under binders. (After all, to quote Olin, "binders 
dominate references.")

Dave