Certified symbolic manipulation: Bivariate simplicial polynomialsModos de exclusión de las mujeres en la sociedad actual

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

    Universidad de Sevilla

    Sevilla, España

    GRID grid.9224.d

  2. 2 Universidad de La Rioja

    Universidad de La Rioja

    Logroño, España

    GRID grid.119021.a

Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC

ISBN: 9781450320597

Year of publication: 2013

Pages: 243-250

Type: Book chapter

Export: RIS
DOI: 10.1145/2465506.2465515 SCOPUS: 2-s2.0-84882248422 lock_openOpen access editor
bar_chart See metrics


Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suita- bly interpreted, ensure the correctness of the algorithms. In this paper, we focus on algebraic algorithms implemented in the proof assistant ACL2, which allows us to verify correct- ness in the same programming environment. The case study is that of bivariate simplicial polynomials, a data structure used to help the proof of properties in Simplicial Topology. Simplicial polynomials can be computationally interpreted in two ways. As symbolic expressions, they can be handled algorithmically, increasing the automation in ACL2 proofs. As representations of functional operators, they help proving properties of categorical morphisms. As an application of this second view, we present the definition in ACL2 of some morphisms involved in the Eilenberg-Zilber reduction, a cen- tral part of the Kenzo computer algebra system. We have proved the ACL2 implementations are correct and tested that they get the same results as Kenzo does. Copyright 2013 ACM.