从 Coq 到传值调用 λ-演算的带时间界认证提取
计算机科学中的逻辑
2022-12-09 v2 编程语言
摘要
我们提供一个插件，将简单多态类型的 Coq 函数提取到（无类型的）传值调用（call-by-value）λ-演算 L。该插件在 MetaCoq 框架中实现，并完全用 Coq 编写。我们提供 Ltac 策略，以依据连接 Coq 函数与正确提取及时间界的逻辑关系自动验证提取项，本质上执行一种认证翻译与运行时间验证。我们给出三个案例研究：由 Coq 对 \L 的步索引自解释器的定义提取而得的通用 L 项；从丢番图方程可解性到 L 的停机问题的多步归约；以及 L 中图灵机的多项式时间模拟。
引用
@article{arxiv.1904.11818,
title = {A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus},
author = {Yannick Forster and Fabian Kunze},
journal= {arXiv preprint arXiv:1904.11818},
year = {2022}
}