Reliably Reproducing Machine-Checked Proofs with the Coq Platform
Karl Palmskog (KTH), Enrico Tassi (STAMP), Th\'eo Zimmermann (PI.R2,, IRIF)
TL;DR
The paper introduces the Coq Platform, a comprehensive distribution of the Coq proof assistant with libraries and tools, facilitating reliable reproduction and extension of formal proofs across research, education, and industry.
Contribution
It details the organization, development process, and comparative advantages of the Coq Platform within the proof assistant community.
Findings
Enables reproducibility of Coq artifacts in various domains
Provides a standardized environment for Coq-based projects
Facilitates comparison with similar proof assistant distributions
Abstract
The Coq Platform is a continuously developed distribution of the Coq proof assistant together with commonly used libraries, plugins, and external tools useful in Coq-based formal verification projects. The Coq Platform enables reproducing and extending Coq artifacts in research, education, and industry, e.g., formalized mathematics and verified software systems. In this paper, we describe the background and motivation for the Platform, and outline its organization and development process. We also compare the Coq Platform to similar distributions and processes in the proof assistant community, such as for Isabelle and Lean, and in the wider open source software community.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Mathematics, Computing, and Information Processing · Security and Verification in Computing