Extend the formalization to shift/reset

[VietAnh1010]

Extend the language and the logical relations with shift/reset. Here are some notable observations:

• To accommodate shift/reset, we introduce meta-context (which plays the role of meta-continuation). Logical relations are extended to include meta-contexts. There are two isomorphic representations of meta-contexts: inside-out and outside-in (just like normal contexts).
• Working with inside-out representations of meta-contexts and contexts is easier when reasoning about small-step execution (inside-out representations mirror exactly the structure of continuations and meta-continuations). For example, to evaluate reset, we cons the current inside-out context to the front of the current inside-out meta-context, and we set the inside-out context to hole. If we work with outside-in representations instead, we need to append the current outside-in context to the back of the current outside-in meta-context, which complicates reasoning.
• Working with outside-in representations of meta-contexts and contexts is easier when reasoning about unique decomposition, as their plug function are structurally recursive without accumulator.
• Proof of unique decomposition is now mostly by equational reasoning. This is achieved by explicitly writing the decomposing function and reasoning with it.
• fmap and bind of outside-in program contexts are corrected, which allows us to write ctxr_comp that composes two program contexts and simplifies reasoning.