A plugin to export Coq libraries to XML

DOI10.1007/978-3-030-23250-4_17zbMath1428.68345OpenAlexW2953556507MaRDI QIDQ2287917

Claudio Sacerdoti Coen

Publication date: 22 January 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-23250-4_17

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Presentation and content markup for mathematics (68V25)

Related Items (1)

Experiences from exporting major proof assistant libraries

Uses Software

• Coq
• Matita
• DeepMath
• CoqHammer
• Logipedia
• SerAPI

This page was built for publication: A plugin to export Coq libraries to XML