Repository logo
  • Log In
    Log in via Symplectic to deposit your publication(s).
Repository logo
  • Communities & Collections
  • Research Outputs
  • Statistics
  • Log In
    Log in via Symplectic to deposit your publication(s).
  1. Home
  2. Faculty of Engineering
  3. Computing
  4. Computing
  5. CoqPyt: Proof navigation in Python in the era of LLMs
 
  • Details
CoqPyt: Proof navigation in Python in the era of LLMs
File(s)
coqpyt.pdf (214.76 KB)
Published version
Author(s)
Carrott, Pedro
Saavedra, Nuno
Thompson, Kyle
Lerner, Sorin
Ferreira, João F
more
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
URI
http://hdl.handle.net/10044/1/116369
URL
https://doi.org/10.1145/3663529.3663814
DOI
https://www.dx.doi.org/10.1145/3663529.3663814
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
https://creativecommons.org/licenses/by/4.0/
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
About
Spiral Depositing with Spiral Publishing with Spiral Symplectic
Contact us
Open access team Report an issue
Other Services
Scholarly Communications Library Services
logo

Imperial College London

South Kensington Campus

London SW7 2AZ, UK

tel: +44 (0)20 7589 5111

Accessibility Modern slavery statement Cookie Policy

Built with DSpace-CRIS software - Extension maintained and optimized by 4Science

  • Cookie settings
  • Privacy policy
  • End User Agreement
  • Send Feedback