SMLtoCoq：从带契约的SML程序自动生成Coq规约与证明义务
计算机科学中的逻辑
2021-07-19 v1 编程语言
摘要
对函数式程序进行形式化推理本应直截了当且优雅，然而通常并未作为惯例进行。在证明辅助工具中推理需在这些工具中“重新实现”代码，这远非易事。SMLtoCoq提供从SML程序与函数契约到Coq的自动翻译。程序被译为Coq规约，函数契约被译为定理，随后可形式化证明。利用Equations插件及其他成熟的Coq库，SMLtoCoq能够翻译不含副作用、包含偏函数、结构、函子、记录等的SML程序。此外，我们提供SML基础库多部分的Coq版本，从而使对这些库的调用几乎原样保留。
引用
@article{arxiv.2107.07664,
title = {SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts},
author = {Laila El-Beheiry and Giselle Reis and Ammar Karkour},
journal= {arXiv preprint arXiv:2107.07664},
year = {2021}
}
备注
In Proceedings LFMTP 2021, arXiv:2107.07376