License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2019.1
URN: urn:nbn:de:0030-drops-130651
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13065/
Go to the corresponding LIPIcs Volume Portal

Kohlhase, Michael ; Rabe, Florian ; Wenzel, Makarius

Making Isabelle Content Accessible in Knowledge Representation Formats

pdf-format:
LIPIcs-TYPES-2019-1.pdf (0.8 MB)

Abstract

The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library into a FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format was already envisioned by the authors in 1999 but had previously proved too difficult.
After substantial improvements of the Isabelle Prover IDE (PIDE) and the OMDoc/Mmt format since then, we are now able to deliver such an export. Concretely we present an integration of PIDE and Mmt that allows exporting all Isabelle libraries in OMDoc format. Our export covers the full Isabelle distribution and the Archive of Formal Proofs (AFP) - more than 12 thousand theories and locales resulting in over 65 GB of OMDoc/XML.
Such a systematic export of Isabelle content to a well-defined interchange format like OMDoc enables many applications such as dependency management, independent proof checking, or library search.

BibTeX - Entry

@InProceedings{kohlhase_et_al:LIPIcs:2020:13065,
  author =	{Michael Kohlhase and Florian Rabe and Makarius Wenzel},
  title =	{{Making Isabelle Content Accessible in Knowledge Representation Formats}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{1:1--1:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Marc Bezem and Assia Mahboubi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13065},
  URN =		{urn:nbn:de:0030-drops-130651},
  doi =		{10.4230/LIPIcs.TYPES.2019.1},
  annote =	{Keywords: Isabelle, PIDE, OMDoc, MMT, library, export}
}

Keywords: Isabelle, PIDE, OMDoc, MMT, library, export
Collection: 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Issue Date: 2020
Date of publication: 24.09.2020
Supplementary Material: The translated libraries are available at https://gl.mathhub.info/Isabelle as compressed OMDoc files.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI