一句话：在 Rocq 中机器化验证带效应的多阶段核心演算 λ_run$，证明类型与展开可靠性和阶段区分。
多阶段编程语言（如 MetaML）具有微妙的语义，许多常见性质在其中不再成立，且与状态、多态等语言特性的交互容易出错；随着通用语言不断引入 MSP 特性，对其设计建立可信性日益紧迫。本文受已有 MSP 系统启发，为一个同时包含编译期与运行期阶段、并带有效应的核心演算 λ_run$ 给出 Rocq（Coq）机器化形式化，覆盖其类型系统、展开（elaboration）与求值语义。作者形式化地建立了类型可靠性、展开可靠性以及阶段区分（phase distinction）等关键性质。该机器化语义旨在为其他 MSP 设计的形式研究提供基础，降低为现有语言扩展 MSP 支持的验证门槛。
Multi-stage programming (MSP) languages such as MetaML have subtle semantics, in which familiar properties often fail to hold and hazardous interactions with other language features such as state or polymorphism abound. The ongoing incorporation of MSP features into general purpose languages makes the need to establish confidence in their design increasingly pressing. Taking inspiration from existing MSP systems, we present a Rocq mechanisation of a core calculus for compile-time and run-time MSP with effects, λ run $ , formally establishing key properties such as type and elaboration soundness and phase distinction. We hope that our mechanised semantics will be a useful basis for formal study of other designs, easing the extension of existing languages with support for MSP.
@article{paperbot3821,
title = {Mechanised Semantics of Multi-stage Programming},
author = {Ka Wing Li and Maite Kramarz and Ningning Xie and Jeremy Yallop},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798260}
}