Sharing Arithmetic Proofs from Dedukti to HOL

François Thiré

Today, we observe a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to co-operate because they do not implement the same logic. Logical frameworks are a class of theorems provers that overcome this issue by their capacity of implementing various logics. In this work, we study the STT∀ βδ logic, an extension of the Simple Type Theory that has been en- coded in the logical framework Dedukti [1]. We show that this new logic is a good candidate to export proofs to other provers. As an example, we show how this logic has been encoded into Dedukti and how we used it to export proof to the HOL family provers via OpenTheory [2] but also to the Coq system

1. Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In Rocca, S.R.D., ed.: Typed Lambda Calculi and Applications, 8th In- ternational Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings. Volume 4583 of Lecture Notes in Computer Science., Springer (2007) 102–117

2. Hurd, J.: The OpenTheory standard theory library. In Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R., eds.: Third International Symposium on NASA Formal Methods (NFM 2011). Volume 6617 of Lecture Notes in Computer Science., Springer (April 2011) 177–191