Update operational semantics to impose one-shot continuations

The operational semantics is modified so that the continuation captured by a TryWith construct can be called at most once by the handler. The idea for accomplishing this is to extend the continuation with a piece of mutable state, which is initialised to true and updated to false after the first call. Moreover, in order to resume a continuation, the state must be true.

Effectively, this is done by extending the continuation constructor ContV with an extra argument l : loc, which represents a memory location. So, to recapitulate, now a continuation ContV k l is the given of a evaluation context k and a memory location l. Furthermore, we modify the reduction rules for both the resumption of a continuation and the capture of a raising effect. Indeed, now, when an effect is captured, the handler is called with a continuation built with a newly allocated memory location initialised to true:

(TryWith (Eff v k) h r); σ → (h v (ContV k l)); σ[l ↦ true]

and a continuation can only be called when this location points to true:

((ContV k l) w); σ[l ↦ true] → (k[w]); σ[l ↦ false]

Finally, we have also adapted some of the proofs to work with this new semantics, but all of the previous definitions and statements remain valid.