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

Any de publicació: 2008

Volum: 5144 LNAI

Número: 5144

Pàgines: 270-284

Tipus: Article

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

Altres publicacions en: Lecture Notes in Computer Science

Projectes relacionats

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

2006/00092/001

Resum

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.