Verifying Selective CPS Transformation for Shift and Reset.

A selective CPS transformation enables us to execute a program with delimited control operators, \\(\\texttt {shift}\\) and \\(\\texttt {reset}\\), in a standard functional language without support for control operators. The selective CPS transformation dispatches not only on the structure of the input term but also its purity: it transforms only those parts that actually involve control effects. As such, the selective CPS transformation consists of many rules, each for one possible combination of the purity of subterms, making its verification tedious and error-prone. In this paper, we first formalize a monomorphic version of the selective CPS transformation in the Agda proof assistant. We use intrinsically typed term and context representations together with parameterized higher-order abstract syntax (PHOAS) to represent binding structures. We then prove the correctness of the transformation, i.e., the equality of terms is preserved by the CPS transformation. Through the formalization, we confirmed that all the rules of the selective CPS transformation in the previous work are correct, but found that one lemma on the behavior of \\(\\texttt {shift}\\) was not precise.