Reseña: “Certified symbolic manipulation: Bivariate simplicial polynomials”
Se ha publicado un artículo de verificación formal en ACL2 titulado Certified symbolic manipulation: Bivariate simplicial polynomials.
Sus autores son Laureano Lambán, Francisco Jesús Martín Mateos, Julio Rubio y José Luis Ruiz Reina.
El trabajo se presentará en el ISSAC 2013 (38th International Symposium on Symbolic and Algebraic Computation).
Su resumen es
Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably 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 correctness 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 central 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.
El código ACL2 de la formalización del teorema de Eilenberg-Zilber se encuentra aquí.