ACL2 verification of simplicial degeneracy programs in the Kenzo system

  1. Martín-Mateos, F.-J. 1
  2. Rubio, J. 2
  3. Ruiz-Reina, J.-L. 1
  1. 1 Universidad de Sevilla
    info

    Universidad de Sevilla

    Sevilla, España

    ROR https://ror.org/03yxnpp24

  2. 2 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Libro:
Intelligent Computer Mathematics

Editorial: SPRINGER-VERLAG

ISBN: 978-3-642-02614-0

Año de publicación: 2009

Volumen: 5625 LNAI

Páginas: 106-121

Tipo: Capítulo de Libro

DOI: 10.1007/978-3-642-02614-0_13 SCOPUS: 2-s2.0-69049092797 GOOGLE SCHOLAR

Resumen

Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It is a descendant of a previous system called EAT (for Effective Algebraic Topology). Kenzo shows a much better performance than EAT due, among other reasons, to a smart encoding of degeneracy lists as integers. In this paper, we give a complete automated proof of the correctness of this encoding used in Kenzo. The proof is carried out using ACL2, a system for proving properties of programs written in (a subset of) Common Lisp. The most interesting idea, from a methodological point of view, is our use of EAT to build a model on which the verification is carried out. Thus, EAT, which is logically simpler but less efficient than Kenzo, acts as a mathematical model and then Kenzo is formally verified against it. © 2009 Springer-Verlag Berlin Heidelberg.