Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
-
1
Universidad de La Rioja
info
ISSN: 0302-9743
Year of publication: 2008
Volume: 5144 LNAI
Issue: 5144
Pages: 270-284
Type: Article
More publications in: Lecture Notes in Computer Science
Related Projects
Abstract
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.