Coqatoo: Generating Natural Language Versions of Coq Proofs

2017/12/11 by Andrew Bedford, Bedford, Andrew
Business, Management and Accounting · Computer Science · #Business Process Modeling and Analysis #FOS: Computer and information sciences #Logic, programming, and type systems #Programming Languages (cs.PL) #Semantic Web and Ontologies #cs.PL

paper · pdf · doi:10.48550/arxiv.1712.03894

International Workshop on Coq for Programming Languages (CoqPL 2018)

arxiv created 2017/12/11 · openalex publication_date 2017/12/11 · arxiv updated 2017/12/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• Reliably Reproducing Machine-Checked Proofs with the Coq Platform
• Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
• Recycling Proof Patterns in Coq: Case Studies
• Machine Learning of Coq Proof Guidance: First Experiments
• Learning how to Prove: From the Coq Proof Assistant to Textbook Style