Foundation of Meta-Programming

这个为期四年的项目的主要目的是学习元编程的基础，也就是编写一个生成程序的程序。元程序设计普遍存在于软件的各个领域，特别是特定领域的语言中，因此，高效、可靠地构建元程序是当今计算机科学中的一个重要问题。在这项研究中，我们观察到对元程序的适当处理需要明确地分离程序的两个控制流，一个用于代码生成，另一个用于生成的代码的执行。为了显式地操纵这些控制流，并将它们抽象为有界的连续，我们研究了两组最重要的控制算子，“移位/重置”和“控制/提示”，并为它们构造了刚性的基础。在对它们进行语义分析的基础上，(1)给出了它们的类型系统；(2)证明了它们与CPS翻译的类型可靠性、合流性、兼容性等基本性质；(3)分析了它们的表达能力。我们相信，这些结果为未来元编程的研究奠定了坚实的基础。

The main purpose of this four-year project is to study the foundation of meta-programming, that is, writing a program that generates programs. Meta-programming is ubiquitous in various fields of software, in particular, domain-specific languages, and, therefore, the efficient and reliable construction of meta-programs is an important issue in today's computer science. In this study, we have observed that a proper treatment of meta-programs needs a clear separation of two control flows of programs, one for the code generation, and the other for the execution of the generated codes. In order to explicitly manipulate these control flows, and abstract them as delimited continuations, we have studied two most important sets of control operators, "shift/reset" and "control/prompt", and constructed rigid foundation for them. Based on the semantical analysis for them, we have (1) given type systems for them, (2) proved basic properties such as type soundness, confluence, and compatibility with CPS translation, and (3) analyzed the expressive power of them. We believe that these results build a solid foundation for the future study of meta-programming.