A Modal Analysis of Staged Computation

We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of functional languages. Our main technical result is a conservative embedding of Nielson & Nielson's two-level functional language in our language Mini-ML 2 , which in addition to partial evaluation also supports multiple computation stages, sharing of code across multiple stages, and run-time code generation. This research was sponsored by the Defense Advance Research Project Agency, CSTO, under the title "The Fox Project: Advanced Development of Systems Software", ARPA Order No. 8313, issued by ESD/AVS under Contract No. F19628-91-C-0168. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the U.S. Government. Keywords: Modal Logic, Two Level Lang..