受控执行的代数语义：幺半群范畴、效应代数和邻接边界

我们提出了一种受控执行的代数语义，其中治理是公理化的、组合的并且与可表达性相联系。该框架由 32 个 Rocq 模块（约 12,000 行、454 个定理、0 个承认）机械化，建立在交互树和参数化共归纳的基础上。三公理治理代数记录（安全性、透明性、适当性）引入了一个具有经过验证的五边形、三角形和六边形一致性的对称幺半群范畴，其中每个张量组合都保留了治理。代数效应系统约束处理程序代数，以便在安全片段中只能构造治理保留处理程序；空能力集中的程序可以证明仅发出可观察性指令。能力索引组合将程序与机器检查的能力界限捆绑在一起，并且双重保证定理确定 inside_caps 和 gov_safe 在所有组合运算符下同时成立。顶点结果是共同边界：在我们的形式模型中，每个可通过四个原始态射构造函数表达的程序都在解释下受控，并且每个受控程序都是此类程序的图像。图灵完备性在治理中得以保留；非中介 I/O 被排除在受控片段之外。治理否认被建模为安全共归纳分歧。治理代数是参数化的：任何实例化三个公理的系统都会继承所有派生属性，包括收敛、组合闭包和目标保留。提取的 OCaml 在 BEAM 运行时中作为 NIF 运行，并通过基于属性的测试（70,000 多个随机输入，零分歧）确认规范和运行时解释器之间的行为等效性。