Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems

DOI10.1007/978-3-540-85110-3_23MaRDI QIDQ5505507zbMATH OpenOpenAlexFDO

Authors César Domínguez

Publication date 27 January 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85110-3_23

zbMATH Keywords

Coq proof assistanthidden algebrassymbolic computation

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 2000439
• Object oriented institutions to specify symbolic computation systems
• Effective homology of bicomplexes, formalized in Coq
• Developing the algebraic hierarchy with type classes in Coq
• Computing in Coq with infinite algebraic data structures

Cites work

• A Declarative Language for the Coq Proof Assistant
• A hidden agenda
• A hidden Herbrand theorem: Combining the object and logic paradigms
• A mechanized proof of the basic perturbation lemma
• An object-oriented interpretation of the EAT system
• Constructive algebraic topology
• Executing in Common Lisp, Proving in ACL2
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• scientific article; zbMATH DE number 2079846 (Why is no real title available?)
• scientific article; zbMATH DE number 1507195 (Why is no real title available?)
• scientific article; zbMATH DE number 1424016 (Why is no real title available?)
• Institutions: abstract model theory for specification and programming
• Object oriented institutions to specify symbolic computation systems
• Specification of abstract data types
• Towards Constructive Homological Algebra in Type Theory

Cited in

(11)

• Formalizing implicative algebras in Coq
• Algebraic-coalgebraic specification in CoCASL
• scientific article; zbMATH DE number 1670755 (Why is no real title available?)
• Embedding of Systems of Affine Recurrence Equations in Coq
• ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
• scientific article; zbMATH DE number 1189281 (Why is no real title available?)
• scientific article; zbMATH DE number 1070623 (Why is no real title available?)
• scientific article; zbMATH DE number 2000439 (Why is no real title available?)
• scientific article; zbMATH DE number 1497880 (Why is no real title available?)
• Object oriented institutions to specify symbolic computation systems
• A case-study in algebraic manipulation using mechanized reasoning tools

Describes a project that uses

Uses Software

• Kenzo
• Coq

This page was built for publication: Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5505507)