CoqPyt: Proof navigation in Python in the era of LLMs
File(s)coqpyt.pdf (214.76 KB)
Published version
Author(s)
Type
Conference Paper
Abstract
Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most of the proof burden on the user, making formal verification a complex, and time-consuming endeavor. Recent automation techniques based on neural methods address this issue, but require good programmatic support for collecting data and interacting with proof assistants. This paper presents CoqPyt, a Python tool for interacting with the Coq proof assistant. CoqPyt improves on other Coq-related tools by providing novel features, such as the extraction of rich premise data. We expect our work to aid development of tools and techniques, especially LLM-based, designed for proof synthesis and repair. A video describing and demonstrating CoqPyt is available at: https://youtu.be/fk74o0rePM8.
Date Issued
2024-07-10
Date Acceptance
2024-07-01
Citation
FSE 2024: Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, 2024, pp.637-641
ISBN
9798400706585
Publisher
ACM
Start Page
637
End Page
641
Journal / Book Title
FSE 2024: Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering
Copyright Statement
Copyright © 2024 Owner/Author. This work is licensed under a Creative Commons Attribution International 4.0 License (https://creativecommons.org/licenses/by/4.0/)
License URL
Identifier
https://doi.org/10.1145/3663529.3663814
Source
FSE '24: 32nd ACM International Conference on the Foundations of Software Engineering
Publication Status
Published
Start Date
2024-07-15
Finish Date
2024-07-19
Coverage Spatial
Porto de Galinhas, Brazil
Date Publish Online
2024-07-10