Verifying Selective CPS Transformation for Shift and Reset

Autor:	Kenichi Asai, Chiaki Ishio
Rok vydání:	2020
Předmět:	Algebra Functional programming TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Correctness Computer science Agda TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Abstract syntax Proof assistant Lemma (logic) Parameterized complexity computer computer.programming_language
Zdroj:	Lecture Notes in Computer Science ISBN: 9783030471460 TFP
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::4efcde1c631b96225a1c5df7a8bd1790 https://doi.org/10.1007/978-3-030-47147-7_3 Zobrazit plný text záznamu