一句话：在 Coq 内构建认证提取管线，将依赖类型程序翻译为多种函数式语言并验证关键变换。
本文解决如何从 Coq 可靠地提取函数式程序到多种目标语言，并尽量缩小可信计算基。作者基于 MetaCoq 的认证擦除，扩展其输出语言加入类型信息，得到中间表示 λ^T_□；围绕该表示实现包含 eta-展开、内联等证明生成式变换以及经验证的未用参数消除优化的完整管线，并针对函数式语言的值调用操作语义证明该优化正确。管线可将优化后的表示 pretty-print 为 Liquidity、CameLIGO、Elm 以及 Rust 子集；在 ConCert 框架中提取了董事会投票和托管两个经验证的真实智能合约，并开发经验证 Web 应用提取为 Elm。可信基仅保留 MetaCoq 与各目标语言 pretty-printer。
Abstract We implement extraction of Coq programs to functional languages based on MetaCoq’s certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call ${\lambda^T_\square}$ . We complement the extraction functionality with a full pipeline that includes several standard transformations (e.g. eta-expansion and inlining) implemented in a proof-generating manner along with a verified optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. From the optimised ${\lambda^T_\square}$ representation, we obtain code in two functional smart contract languages, Liquidity and CameLIGO, the functional language Elm, and a subset of the multi-paradigm language for systems programming Rust. Rust is currently gaining popularity as a language for smart contracts, and we demonstrate how our extraction can be used to extract smart contract code for the Concordium network. The development is done in the context of the ConCert framework that enables smart contract verification. We contribute with two verified real-world smart contracts (boardroom voting and escrow), which we use, among other examples, to exemplify the applicability of the pipeline. In addition, we develop a verified web application and extract it to fully functional Elm code. In total, this gives us a way to write dependently typed programs in Coq, verify, and then extract them to several target languages while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.
@article{paperbot1635,
title = {Extracting functional programs from Coq, in Coq},
author = {DANIL ANNENKOV and MIKKEL MILO and JAKOB BOTSCH NIELSEN and BAS SPITTERS},
journal = {Journal of Functional Programming},
volume = {32},
year = {2022},
doi = {10.1017/s0956796822000077}
}