Coqatoo: Generating Natural Language Versions of Coq Proofs
Programming Languages
2017-12-12 v1
Abstract
Due to their numerous advantages, formal proofs and proof assistants, such as Coq, are becoming increasingly popular. However, one disadvantage of using proof assistants is that the resulting proofs can sometimes be hard to read and understand, particularly for less-experienced users. To address this issue, we have implemented a tool capable of generating natural language versions of Coq proofs called Coqatoo, which we present in this paper.
Cite
@article{arxiv.1712.03894,
title = {Coqatoo: Generating Natural Language Versions of Coq Proofs},
author = {Andrew Bedford},
journal= {arXiv preprint arXiv:1712.03894},
year = {2017}
}
Comments
International Workshop on Coq for Programming Languages (CoqPL 2018)