Reliably Reproducing Machine-Checked Proofs with the Coq Platform - INRIA - Institut National de Recherche en Informatique et en Automatique Access content directly
Preprints, Working Papers, ... Year : 2022

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 verification projects. The Coq Platform enables reproducing and extending Coq-based 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 and wider open source software community.
Fichier principal
Vignette du fichier
main.pdf (211.46 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03592675 , version 1 (01-03-2022)
hal-03592675 , version 2 (18-03-2022)

Identifiers

  • HAL Id : hal-03592675 , version 1

Cite

Karl Palmskog, Enrico Tassi, Théo Zimmermann. Reliably Reproducing Machine-Checked Proofs with the Coq Platform. 2022. ⟨hal-03592675v1⟩
250 View
224 Download

Share

Gmail Facebook X LinkedIn More