A Plugin to Export Coq Libraries to XML
Springer Verlag, 2019
Online
Konferenz
Zugriff:
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.
Titel: |
A Plugin to Export Coq Libraries to XML
|
---|---|
Autor/in / Beteiligte Person: | Sacerdoti Coen C. |
Link: | |
Veröffentlichung: | Springer Verlag, 2019 |
Medientyp: | Konferenz |
DOI: | 10.1007/978-3-030-23250-4_17 |
Schlagwort: |
|
Sonstiges: |
|