Paper Info
Title
Focalize And Dedukti To The Rescue For Proof Interoperability
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 Math-Transfer. We finally illustrate this methodology on the Sieve of Eratosthenes, which we prove correct using HOL and Coq in combination.
Year
DOI
Venue
2017
10.1007/978-3-319-66107-0_9
INTERACTIVE THEOREM PROVING (ITP 2017)
Field
DocType
Volume
Sieve of Eratosthenes,HOL,Parameterized complexity,Programming language,Computer science,Interoperability,Algorithm,Mathematical proof,Formalism (philosophy),Logical framework,Pointwise
Conference
10499
ISSN
Citations 
PageRank 
0302-9743
1
0.40
References 
Authors
15
2
Name
Order
Citations
PageRank
Raphaël Cauderlier1153.08
Catherine Dubois2346.26