By Yuse Yoshihiro and Atsushi Igarashi. In Proceedings of the 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, pages 201-212, Venice, Italy, July 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 stages---naturally arises. In this paper we propose a typed lambda calculus λCB, 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 $\C A$ (next $A$) to a type of code that runs at the next stage; and (3) a formula $\B A$ (always $A$) to a type of persistent code executable at and after the current stage. After formalizing \(\lambdaCB\), 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.
$Date: 2006-07-17 20:48:26 +0900 (Mon, 17 Jul 2006) $