Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems

  1. Domínguez, C. 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: 2008

Volumen: 5144 LNAI

Número: 5144

Páginas: 270-284

Tipo: Artículo

DOI: 10.1007/978-3-540-85110-3_23 SCOPUS: 2-s2.0-51049117567 WoS: WOS:000258392600022 GOOGLE SCHOLAR

Otras publicaciones en: Lecture Notes in Computer Science

Proyectos relacionados

Sistemas de cálculo simbólico: nuevos desarrollos en topología algebráica y fiabilidad

2006/00092/001

Resumen

This work is an attempt to formalize, using the Coq proof assistant, the algebraic specification of the data structures appearing in two symbolic computation systems for algebraic topology called EAT and Kenzo. The specification of these structures have been obtained through an operation, called imp operation, between different specification frameworks as standard algebraic specifications and hidden specifications. Reusing previous Coq implementations of universal algebra and category theory we have proposed a Coq formalization of the imp operation, extending the representation to the particular hidden algebras which take part in this operation. © 2008 Springer-Verlag Berlin Heidelberg.