Logical Modalities and Multi-Stage Programming
Zine-el-Abidine Benaissa, Eugenio Moggi, Walid Taha, Tim Sheard · 1999
. Multi-stage programming is a method for improving the performance of programs through the introduction of controlled program specialization. This paper makes a case for multi-stage programming with open code and closed values. We argue that a simple language exploiting interactions between two logical modalities is well suited for multi-stage programming, and report the results from our study of categorical models for multi-stage languages. Keywords: Multi-stage programming, categorical models, semantics, type systems #multi-level typed calculi #, combination of logics #modal and temporal#. 1 Introduction Multi-stage programming is a method for improving the performance of programs through the introduction of controlled program specialization #15, 13#. MetaML was the #rst language designed speci#cally to support this method. It provides a type constructor for #code" and staging annotations for building, combining, and executing code, thus allowing the programmer to have #ner control...