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

Journal:
Lecture Notes in Computer Science

ISSN: 0302-9743

Year of publication: 2014

Volume: 8884

Pages: 49-63

Type: Article

SCOPUS: 2-s2.0-84917740632 GOOGLE SCHOLAR

More publications in: Lecture Notes in Computer Science

Abstract

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.