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

Aldizkaria:
Lecture Notes in Computer Science

ISSN: 0302-9743

Argitalpen urtea: 2008

Alea: 5144 LNAI

Zenbakia: 5144

Orrialdeak: 270-284

Mota: Artikulua

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

Beste argitalpen batzuk: Lecture Notes in Computer Science

Lotura duten proiektuak

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

2006/00092/001

Laburpena

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.