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, syntactically, 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 to a deeply embedded 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 adversarial contexts. This goes beyond the state of the art in verified and certifying extraction, which so far has focused on correctness rather than security.

翻译：使用单子表示效应的浅层嵌入在面向证明的语言中广受欢迎，因为它们便于形式化验证。浅层嵌入程序一旦被验证，通常会被提取至OCaml或C等主流语言，并链接到更大的代码库中。提取过程并未完全验证，因为它常涉及引用——将浅层嵌入程序转换为深层嵌入程序——而验证引用仍是一个重大的开放挑战。为此，先前的一些工作通过翻译验证来认证个别提取结果，从而获得形式化正确性保证。我们基于这一思路，但将翻译验证的使用限制在首次提取步骤中，我们称之为关系引用，该步骤使用元程序为给定的浅层嵌入程序构建类型推导。由于类型推导遵循原始程序的结构，该元程序较为简单。一旦我们在语法上验证了类型推导对原始程序有效，便将其传递给已验证的语法生成函数，该函数生成的代码保证与原始程序在语义上相关。我们应用这一通用思想构建了SEIO*，一个将带IO的浅层嵌入F*程序提取至深层嵌入λ演算的框架，同时提供形式化的安全编译保证。利用两个跨语言逻辑关系，我们在F*中设计了机器可检查的证明，表明SEIO*保证鲁棒关系超属性保持（RrHP），这是一种非常强大的安全编译标准，蕴含完全抽象性，以及对任意对抗上下文的迹属性和超属性的保持。这超越了当前已验证和认证提取的研究现状，后者迄今主要关注正确性而非安全性。