Actually, no... I don't think what you're describing is quite what I was thinking of originally. But whatever its behavior is, it makes sense.
The difference, I guess, is that in the stack-popping model, before doesn't always propagate past lambda. It only affects variable accesses that would be "free" if the thing inside before stood as an expression on its own.

Ah, that makes sense. I was thinking about something like that. What you describe seems equivalent to propagating an extra before into each variable expression, which I had considered but dismissed as too ad hoc. Your explanation makes much clearer what's going on and why this is sensible behavior. Thanks!

I'm a little confused about the interface described in Language -- it seems to indicate that nonsensical programs such as before (lambda here) are allowed, and the example tests don't say anything about such programs. Do I need to read the paper to figure out how to handle these, or are they just supposed to crash?