Reliably Reproducing Machine-Checked Proofs with the Coq Platform - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Reliably Reproducing Machine-Checked Proofs with the Coq Platform

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (141.91 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Identifiants

Citer

Karl Palmskog, Enrico Tassi, Théo Zimmermann. Reliably Reproducing Machine-Checked Proofs with the Coq Platform. RRRR 2022 - Workshop on Reproducibility and Replication of Research Results, Apr 2022, Munich, Germany. ⟨hal-03592675v2⟩
248 Consultations
222 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More