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

Revue:
Lecture Notes in Computer Science

ISSN: 0302-9743

Année de publication: 2008

Volumen: 5144 LNAI

Número: 5144

Pages: 270-284

Type: Article

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

D'autres publications dans: Lecture Notes in Computer Science

Projets liés

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

2006/00092/001

Résumé

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.