Top

Published in:

2019 | OriginalPaper | Chapter

The Coq Library as a Theory Graph

Authors : Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen

Published in: Intelligent Computer Mathematics

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

Representing proof assistant libraries in a way that allows further processing in other systems is becoming increasingly important. It is a critical missing link for integrating proof assistants both with each other or with peripheral tools such as IDEs or proof checkers. Such representations cannot be generated from library source files because they lack semantic enrichment (inferred types, etc.) and only the original proof assistant is able to process them. But even when using the proof assistant’s internal data structures, the complexities of logic, implementation, and library still make this very difficult.

We describe one such representation, namely for the library of Coq, using OMDoc theory graphs as the target format. Coq is arguably the most formidable of all proof assistant libraries to tackle, and our work makes a significant step forward.

On the theoretical side, our main contribution is a translation of the Coq module system into theory graphs. This greatly reduces the complexity of the library as the more arcane module system features are eliminated while preserving most of the structure. On the practical side, our main contribution is an implementation of this translation. It takes the entire Coq library, which is split over hundreds of decentralized repositories, and produces easily-reusable OMDoc files as output.

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 Formalization of Dubé’s Degree Bounds for Gröbner Bases in Isabelle/HOL

next chapter BNF-Style Notation as It Is Actually Used

Available online at https://kwarc.info/people/dmueller/pubs/CoqImport.pdf.

[APS+03]

Asperti, A., Padovani, L., Sacerdoti Coen, C., Guidi, F., Schena, I.: Mathematical knowledge management in HELM. Ann. Math. Artif. Intell. 38(1–3), 27–46 (2003)MathSciNetMATHCrossRef

[ARCT11]

Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The matita interactive theorem prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 64–69. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_7CrossRef

[Ass15]

Assaf, A.: A framework for defining computational higher-order logics. Ph.D. thesis, École Polytechnique (2015)

[BB12]

Boespflug, M., Burel, G.: CoqInE: translating the calculus of inductive constructions into the lambda pi-calculus modulo. In: Pichardie, D., Weber, T. (eds.) Proof Exchange for Theorem Proving (2012)

[BCH12]

Boespflug, M., Carbonneaux, Q., Hermant, O.: The \(\lambda \Pi \)-calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp. 28–43 (2012)

[CHK+12]

Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F.: A proof theoretic interpretation of model theoretic hiding. In: Mossakowski, T., Kreowski, H.-J. (eds.) WADT 2010. LNCS, vol. 7137, pp. 118–138. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28412-0_9MATHCrossRef

[CK18]

Czajka, L., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61(1–4), 423–453 (2018)MathSciNetMATHCrossRef

[CMR16]

Codescu, M., Mossakowski, T., Rabe, F.: Selecting colimits for parameterisation and networks of specifications. In: Roggenbach, M., James, P. (eds.) Workshop on Algebraic Development Techniques (2016)

[Coq15]

Coq Development Team: The Coq proof assistant: reference manual. Technical report, INRIA (2015)

[GGMR09]

Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_23CrossRef

[HHP93]

Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143–184 (1993)MathSciNetMATHCrossRef

[IKRU13]

Iancu, M., Kohlhase, M., Rabe, F., Urban, J.: The Mizar mathematical library in OMDoc: translation and applications. J. Autom. Reason. 50(2), 191–202 (2013)MathSciNetMATHCrossRef

[KMOR17]

Kohlhase, M., Müller, D., Owre, S., Rabe, F.: Making PVS accessible to generic services by interpretation in a universal format. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 319–335. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66107-0_21CrossRef

[KR14]

Kaliszyk, C., Rabe, F.: Towards knowledge management for HOL light. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 357–372. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_26CrossRef

[KR16]

Kohlhase, M., Rabe, F.: QED reloaded: towards a pluralistic formal library of mathematical knowledge. J. Formaliz. Reason. 9(1), 201–234 (2016)MathSciNet

[KW10]

Keller, C., Werner, B.: Importing HOL light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307–322. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_22CrossRef

[MAH06]

Mossakowski, T., Autexier, S., Hutter, D.: Development graphs - proof management for structured specifications. J. Log. Algebr. Program. 67(1–2), 114–145 (2006)MathSciNetMATHCrossRef

[oFD18]

European Commission Expert Group on FAIR Data: Turning fair into reality (2018). https://doi.org/10.2777/1524

[OS06]

Obua, S., Skalberg, S.: Importing HOL into Isabelle/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 298–302. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_27CrossRef

[Rab17]

Rabe, F.: How to identify, translate, and combine logics? J. Logic Comput. 27(6), 1753–1798 (2017)MathSciNetMATHCrossRef

[Rab18]

Rabe, F.: A modular type reconstruction algorithm. ACM Trans. Comput. Logic 19(4), 1–43 (2018)MathSciNetMATHCrossRef

[RK13]

Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230(1), 1–54 (2013)MathSciNetMATHCrossRef

[Sac19]

Sacerdoti Coen, S.: A plugin to export Coq libraries to XML. In: 12th International Conference on Intelligent Computer Mathematics, CICM 2019. Lecture Notes in Artificial Intelligence (2019)

Title: The Coq Library as a Theory Graph
Authors: Dennis Müller
Florian Rabe
Claudio Sacerdoti Coen
Publisher: Springer International Publishing
Book: Intelligent Computer Mathematics
Print ISBN: 978-3-030-23249-8

Electronic ISBN: 978-3-030-23250-4

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-23250-4_12

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner