Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems

DOI10.1007/978-3-540-85110-3_23zbMath1166.68373OpenAlexW1516788060MaRDI QIDQ5505507

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

symbolic computationCoq proof assistanthidden algebras

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Related Items (2)

A case-study in algebraic manipulation using mechanized reasoning tools ⋮ ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System

Uses Software

• Coq
• Kenzo

Cites Work

• A mechanized proof of the basic perturbation lemma
• An object-oriented interpretation of the EAT system
• A hidden agenda
• Constructive algebraic topology
• A hidden Herbrand theorem: Combining the object and logic paradigms
• A Declarative Language for the Coq Proof Assistant
• Institutions: abstract model theory for specification and programming
• Executing in Common Lisp, Proving in ACL2
• Towards Constructive Homological Algebra in Type Theory
• Object oriented institutions to specify symbolic computation systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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