A modal type system for multi-level generating extensions with persistent code
Yosihiro Yuse, Atsushi Igarashi · 2006
Multi-level generating extensions, studied by Glück and Jørgensen, are generalization of (two-level) program generators, such as parser generators, to arbitrary many levels. By this generalization, the notion of persistent code—a quoted code fragment that can be used for different levels—naturally arises. In this paper we propose a typed lambda calculus λ©, based on linear-time temporal logic, as a basis of programming languages for multi-level generating extensions with persistent code. The key idea of the type system is correspondence of (1) linearly ordered times in the logic to computation stages; (2) a formula ©A (next A) to a type of code that runs at the next stage; and (3) a formula A (always A) to a type of persistent code executable at and after the current stage. After formalizing λ©, we prove its key property of time-ordered normalization that a well-typed program can never go back to a previous stage in a “time-ordered ” execution, as well as basic properties such as subject reduction, confluence and strong normalization. Commuting conversion plays an important role for time-ordered normalization to hold.