Coqatoo：生成Coq证明的自然语言版本
编程语言
2017-12-12 v1
摘要
由于形式化证明和证明助手（如Coq）的诸多优势，它们正变得越来越流行。然而，使用证明助手的一个缺点是，所产生的证明有时难以阅读和理解，尤其是对经验较少的用户而言。为解决此问题，我们实现了一个能够生成Coq证明自然语言版本的工具，称为Coqatoo，本文即介绍该工具。
引用
@article{arxiv.1712.03894,
title = {Coqatoo: Generating Natural Language Versions of Coq Proofs},
author = {Andrew Bedford},
journal= {arXiv preprint arXiv:1712.03894},
year = {2017}
}
备注
International Workshop on Coq for Programming Languages (CoqPL 2018)