FoCaLiZe and Dedukti to the rescue for proof interoperability

4Citations
Citations of this article
3Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Numerous contributions have been made for some years to allow users to exchange formal proofs between different provers. The main propositions consist in ad hoc pointwise translations, e.g. between HOL Light and Isabelle in the Flyspeck project or uses of more or less complete certificates. We propose in this paper a methodology to combine proofs coming from different theorem provers. This methodology relies on the Dedukti logical framework as a common formalism in which proofs can be translated and combined. To relate the independently developed mathematical libraries used in proof assistants, we rely on the structuring features offered by FoCaLiZe, in particular parameterized modules and inheritance to build a formal library of transfer theorems called MathTransfer. We finally illustrate this methodology on the Sieve of Eratosthenes, which we prove correct using HOL and Coq in combination.

Cite

CITATION STYLE

APA

Cauderlier, R., & Dubois, C. (2017). FoCaLiZe and Dedukti to the rescue for proof interoperability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10499 LNCS, pp. 131–147). Springer Verlag. https://doi.org/10.1007/978-3-319-66107-0_9

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free