Obtaining an ACL2 specification from an Isabelle/HOL theory

  1. Aransay-Azofra, J. 1
  2. Divasón, J. 1
  3. Heras, J. 1
  4. Lambán, L. 1
  5. Pascual, M.V. 1
  6. Rubio, Á.L. 1
  7. Rubio, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Revista:
Lecture Notes in Computer Science

ISSN: 0302-9743

Año de publicación: 2014

Volumen: 8884

Páginas: 49-63

Tipo: Artículo

SCOPUS: 2-s2.0-84917740632 GOOGLE SCHOLAR

Otras publicaciones en: Lecture Notes in Computer Science

Resumen

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.