Reliably Reproducing Machine-Checked Proofs with the Coq Platform
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.
Cite
@article{arxiv.2203.09835,
title = {Reliably Reproducing Machine-Checked Proofs with the Coq Platform},
author = {Karl Palmskog and Enrico Tassi and Théo Zimmermann},
journal= {arXiv preprint arXiv:2203.09835},
year = {2022}
}
Comments
RRRR 2022 - Workshop on Reproducibility and Replication of Research Results, Apr 2022, Munich, Germany