A Logical Foundation for Environment Classifiers
Takeshi Tsukada\rsupera Address: \lsuperaGraduate School of Information Science, Tohoku University Email address: and Atsushi Igarashi\rsuperb Address: \lsuperbGraduate School of Informatics, Kyoto University Email address:
Abstract
Taha and Nielsen have developed a multi-stage calculus $\lambda^{\alpha}$ with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragments and variable declarations are annotated, and their scoping mechanism is used to ensure statically that certain code fragments are closed and safely runnable.
中文速览
多阶段编程需要同时支持开放代码、代码执行和跨阶段嵌入，又要在编译时保证生成的代码封闭且安全，但原有环境分类器系统的类型规则缺少清晰的逻辑基础。作者借助 Curry–Howard 对应，设计了带环境分类器的类型化 λ 演算 λ^▷，把分类器解释为可能世界之间带标签的转换序列，并将 run 和跨阶段持久化统一为分类器应用。该演算满足类型保持、合流性、强正规化和按阶段进行的正规化，还证明良类型程序能安全地分阶段执行，并建立了相应经典逻辑与 Kripke 语义之间的可靠性和完备性。其重要性在于，它把多阶段语言中原本零散、复杂的安全机制统一到一个有逻辑语义支撑的框架里，为 MetaOCaml 一类语言的设计、证明和实现提供了更简洁的基础。
原文 arXiv:1010.3806;中英对照 + 大白话阅读 https://aha.fim.ai/paper/1010.3806v3