Foundation of Programming Languages for Code Generation

本研究项目的目的是将计算效应引入到编程语言中，用于代码生成（或“分段”），以便人们可以自然地编写高效的代码生成器，同时可以保证生成的代码的安全性。作为该项目的研究成果，我们获得了一种具有多提示分隔控制运算符的代码生成语言，证明了类型稳健性，这意味着该语言的安全性，并为我们的语言实现了原型类型解释器和类型推理系统。我们还为代码生成的演算提供了逻辑基础，为分隔控制运算符构建了一个类型导向的部分求值器，并在高性能计算中实现了几个有用的算法，这些都证明了我们语言的实用性和适用性。

The objective of this research project is to introduce computational effect to the programming language for code generation (or “staging”) so that one can write efficient code generators naturally, and at the same time the generated codes can be guaranteed to be safe. As research results of this project, we have obtained a language for code generation with multi-prompt delimited-control operators, proved type soundness which implies the safety of the language, and implemented a proto-type interpreter and a type inference system for our language. We have also given a logical foundation for the calculus of code generation, built a type-directed partial evaluator for delimited-control operators, and implemented several useful algorithms in high-performance computation, which proved usefulness and applicability of our language.