论文标题
出口主要证明助理图书馆的经验
Experiences from Exporting Major Proof Assistant Libraries
论文作者
论文摘要
证明助手的互操作性及其图书馆的整合是在定理证明领域的高度重视但难以捉摸的目标。作为预备步骤，在先前的工作中，我们将多个证明助手的库，特别是Coq，hol Light，Imps，Isabelle，Mizar和PVS的库中：OMDOC/MMT。 每次翻译都提出了巨大的理论，技术和社会挑战，有些是普遍的，有些是特定于系统的，有些可以解决，有些仍然开放。在本文中，我们调查了这些挑战，并比较和评估我们选择的解决方案。 我们认为，类似的图书馆翻译将是任何未来系统互操作性解决方案的重要组成部分，我们的经验将对其他努力的人有价值。
The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented tremendous theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution and our experiences will prove valuable to others undertaking such efforts.
