Obtaining an ACL2 specification from an Isabelle/HOL theory
- Aransay-Azofra, J. 1
- Divasón, J. 1
- Heras, J. 1
- Lambán, L. 1
- Pascual, M.V. 1
- Rubio, Á.L. 1
- Rubio, J. 1
-
1
Universidad de La Rioja
info
ISSN: 0302-9743
Argitalpen urtea: 2014
Alea: 8884
Orrialdeak: 49-63
Mota: Artikulua
Beste argitalpen batzuk: Lecture Notes in Computer Science
Laburpena
In this work, we present an interoperability framework that enables the translation of specifications (signature of functions and lemma statements) among different theorem provers. This translation is based on a new intermediate XML language, called XLL, and is performed almost automatically. As a case study, we focus on porting developments from Isabelle/HOL to ACL2. In particular, we study the transformation to ACL2 of an Isabelle/HOL theory devoted to verify an algorithm computing a diagonal form of an integer matrix (looking for the ACL2 executability that is missed in Isabelle/HOL). Moreover, we provide a formal proof of a fragment of the obtained ACL2 specification — this shows the suitability of our approach to reuse in ACL2 a proof strategy imported from Isabelle/HOL.