Jun Inoue, Verifying Monadically, Memoizingly Staged Programs

Multi-stage programming (MSP) languages provide staging annotations, a natural tool for expressing and/or exploiting phase separations in a computer program. MSP can play two important roles in program analysis and language design: removing overhead associated with straightforward, easy-to-analyze code, like interpreters as opposed to compilers for a domain-specific language, thus making such code practical; and serving as a formal tool for studying languages and systems with natural phase distinction, like hardware description languages.

When done incorrectly, however, staging annotations can severely and unnecessarily inflate the amount of computation in the later phases, or even alter the behavior of a program. An effective approach, monadically memoized staging, has been given as a solution to this problem, but its correctness is yet to be established formally. In fact, we have little prior work on formally reasoning about specific staging methodologies or staged programs. This is less than ideal considering MSP's potential as an aid to program analysis.

We demonstrate two formal results to close this gap, for purely functional programs. We first givea a correctness criterion for a staged program, where correctness is defined to be equivalence with its unstaged counterpart. This is a foundational result that will be useful for verifying almost any staged program correct. We then show how the correctness criterion can be established for programs staged with a certain restriction of the monadically memoized staging method. This restriction of the method applies to a broad range of programs, including many forms of interpreters. Hence our results will automatically establish the correctness of those programs, provided they were correct before being staged.