We introduce a plugin for the interactive prover Coq to export its libraries to a machine readable XML format. The information exported is the one checked by Coq’s kernel after the input is elaborated, augmented with additional data coming from the elaboration itself. The plugin has been applied to the 49 Coq libraries that have an opam package and that currently compile with the latest version of Coq (8.9.0), generating a large dataset of 1,235,934 compressed XML files organized in 18,780 directories that require 17 GB on disk.

A Plugin to Export Coq Libraries to XML

Sacerdoti Coen C.
2019

Abstract

We introduce a plugin for the interactive prover Coq to export its libraries to a machine readable XML format. The information exported is the one checked by Coq’s kernel after the input is elaborated, augmented with additional data coming from the elaboration itself. The plugin has been applied to the 49 Coq libraries that have an opam package and that currently compile with the latest version of Coq (8.9.0), generating a large dataset of 1,235,934 compressed XML files organized in 18,780 directories that require 17 GB on disk.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
243
257
Sacerdoti Coen C.
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11585/698613
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact