A Modal Type System for Multi-Level Generating Extensions with Persistent Code Seminars/Workshops

Abstract

Multi-level generating extensions, studied by Glueck and Jorgensen, 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 (lambdaCB), 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 circ A (next A) to a type of code that runs at the next stage; and (3) a formula Box 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. (Joint work with Yoshihiro Yuse.)