一句话：用关系式引述结合翻译验证，把带 IO 的浅嵌入 F* 程序提取为深嵌入 STLC，并机器验证其满足 RrHP 安全编译准则。
用 monad 表示效应的浅嵌入在证明导向语言中很流行，便于形式验证；但这类程序验证后往往被提取到 OCaml、C 等主流语言并链接进更大代码库。提取过程本身未被完全验证，因为它通常涉及 quotation——把浅嵌入程序变成深嵌入程序，而验证 quotation 仍是公开难题；已有工作只能用翻译验证逐个证明提取结果的正确性。本文把翻译验证限制在第一个提取步骤，称为「关系式引述」：用元程序为给定浅嵌入程序构造类型推导，由于推导结构跟随原程序，元程序很简单；一旦验证该推导对原程序成立，就交给已验证的语法生成函数，产出与原程序语义相关的代码。作者据此构建 SEIO*，将带 IO 与精化类型的浅嵌入 F* 程序提取到深嵌入简单类型 λ 演算。借助两个跨语言逻辑关系，在 F* 中给出机器检验的证明：SEIO* 保证 Robust Relational Hyperproperty Preservation（RrHP），该准则蕴含 full abstraction 以及对任意链接对抗代码的 trace 性质与超性质保持，超越了以往只关注正确性而非安全性的可验证/可证明提取工作。
Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C and linked into larger codebases. The extraction process is not fully verified because it often involves quotation -- turning the shallowly embedded program into a deeply embedded one -- and verifying quotation remains a major open challenge. Instead, some prior work obtains formal correctness guarantees using translation validation to certify individual extraction results. We build on this idea, but limit the use of translation validation to a first extraction step that we call relational quotation and that uses a metaprogram to construct a typing derivation for the given shallowly embedded program. This metaprogram is simple, since the typing derivation follows the structure of the original program. Once we validate that the typing derivation is valid for the original program, we pass it to a verified syntax-generation function that produces code guaranteed to be semantically related to the original program. We apply this general idea to build SEIO*, a framework for extracting shallowly embedded F* programs with IO and refinement types to a deeply embedded simply typed lambda-calculus while providing formal secure compilation guarantees. Using two cross-language logical relations, we devise a machine-checked proof in F* that SEIO* guarantees Robust Relational Hyperproperty Preservation (RrHP), a very strong secure compilation criterion that implies full abstraction as well as preservation of trace properties and hyperproperties against arbitrary linked adversarial code. This goes beyond the state of the art in verified and certifying extraction, which so far has focused on correctness rather than security.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2602-19973,
title = {Misquoted No More: Securely Extracting F* Programs with IO},
author = {Cezar-Constantin Andrici and Abigail Pribisova and Danel Ahman and Cătălin Hrițcu and Exequiel Rivas and Théo Winterhalter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828689}
}