Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Automated Theory Exploration for Interactive Theorem Proving: Read chapter Read first chapter

2017 | Supplement | Chapter

FoCaLiZe and Dedukti to the Rescue for Proof Interoperability

Authors : Raphaël Cauderlier, Catherine Dubois

Published in: Interactive Theorem Proving

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation
next chapter A Formal Proof in Coq of LaSalle’s Invariance Principle
Footnotes
1
The purpose is to illustrate the methodology previously presented. Of course, this example is simple enough to be completely realized within Coq or done by reusing e.g. the translation from Hol Light to Coq proposed by Keller and Werner  [1].
 
2
The Coq Init library is the part of Coq standard library defining logical connectives and basic datatypes such as natural numbers and lists.
 
Literature
1.
Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135–150. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-25379-9_​12CrossRef
2.
Assaf, A.: A framework for defining computational higher-order logics. Ph.D. thesis, École Polytechnique (2015)
3.
Assaf, A., Burel, G.: Translating HOL to Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, EPTCS, Berlin, Germany, 2–3 August 2015, vol. 186, pp. 74–88 (2015)
4.
5.
Assaf, A., Cauderlier, R.: Mixing HOL and Coq in Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) 4th Workshop on Proof eXchange for Theorem Proving, EPTCS, Berlin, Germany, 2–3 August 2015, vol. 186, pp. 89–96 (2015)
6.
Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12–27. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-24364-6_​2CrossRef
7.
8.
Bury, G., Delahaye, D., Doligez, D., Halmagrand, P., Hermant, O.: Automated deduction in the B set theory using typed proof search and deduction modulo. In: LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Suva, Fiji, November 2015
9.
Cauderlier, R.: A rewrite system for proof constructivization. In: Proceedings of the 2016 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, pp. 2:1–2:7. ACM (2016)
10.
Cauderlier, R., Dubois, C.: ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 459–468. Springer, Cham (2016). doi:10.​1007/​978-3-319-46750-4_​26CrossRef
11.
Cauderlier, R., Halmagrand, P.: Checking Zenon modulo proofs in Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings 4th Workshop on Proof eXchange for Theorem Proving, EPTCS, Berlin, Germany, 2–3 August 2015, vol. 186, pp. 57–73 (2015)
12.
13.
Gauthier, T., Kaliszyk, C.: Matching concepts across HOL libraries. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 267–281. Springer, Cham (2014). doi:10.​1007/​978-3-319-08434-3_​20CrossRef
14.
Horozal, F., Rabe, F.: Representing model theory in a type-theoretical logical framework. Theor. Comput. Sci. 412, 4919–4945 (2011)MathSciNetCrossRef
15.
Howe, D.J.: Importing mathematics from HOL into Nuprl. In: Goos, G., Hartmanis, J., Leeuwen, J., Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 267–281. Springer, Heidelberg (1996). doi:10.​1007/​BFb0105410CrossRef
16.
17.
18.
Kaliszyk, C., Krauss, A.: Scalable LCF-style proof translation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving. number 7998 in LNCS, pp. 51–66. Springer, Heidelberg (2013)CrossRef
19.
20.
Miller, D., Certificates, F.P.: Making proof universal and permanent. In: Momigliano, A., Pientka, B., Pollack, R. (eds.) Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, 23 September 2013, pp. 1–2. ACM (2013)
21.
Pessaux, F.: FoCaLiZe: inside an F-IDE. In: Dubois, C., Giannakopoulou, D., Méry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, EPTCS, Grenoble, France, 6 April 6 2014, vol. 149, pp. 64–78 (2014)
22.
Prevosto, V., Jaume, M.: Making proofs in a hierarchy of mathematical structures. In: Proceedings of Calculemus, September 2003
23.
Saillard, R.: Type checking in the Lambda-Pi-Calculus modulo: theory and practice. Ph.D. thesis, MINES Paritech (2015)
24.
Schürmann, C., Stehr, M.-O.: An executable formalization of the HOL/Nuprl connection in the metalogical framework twelf. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 150–166. Springer, Heidelberg (2006). doi:10.​1007/​11916277_​11CrossRef
25.
Wiedijk, F.: Encoding the HOL light logic in Coq (2007, unpublished notes)
26.
Zimmermann, T., Herbelin, H.: Automatic and transparent transfer of theorems along isomorphisms in the coq proof assistant. CoRR, abs/1505.05028 (2015)
Metadata
Title
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability
Authors
Raphaël Cauderlier
Catherine Dubois
Copyright Year
2017
Publisher
Springer International Publishing
Book
Interactive Theorem Proving

Print ISBN: 978-3-319-66106-3

Electronic ISBN: 978-3-319-66107-0

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-66107-0_9

Premium Partner

    Image Credits