Computing in Coq with infinite algebraic data structures

DOI10.1007/978-3-642-14128-7_18MaRDI QIDQ3582708zbMATH OpenOpenAlexFDO

Authors César Domínguez, Julio Rubio

Publication date 24 August 2010

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

Full work available at URL https://doi.org/10.1007/978-3-642-14128-7_18

zbMATH Keywords

computer algebraformal methodsprogram verificationtheorem proving

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Symbolic computation and algebraic computation (68W30)

Recommendations

• Effective homology of bicomplexes, formalized in Coq
• Developing the algebraic hierarchy with type classes in Coq
• A Coq formalization of finitely presented modules
• A constructive algebraic hierarchy in Coq.
• Computing persistent homology within Coq/SSReflect

Cited in

(7)

• A constructive algebraic hierarchy in Coq.
• Formalization of a normalization theorem in simplicial topology
• Modelling algebraic structures and morphisms in ACL2
• A Coq formalization of finitely presented modules
• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• Developing the algebraic hierarchy with type classes in Coq
• Effective homology of bicomplexes, formalized in Coq

Describes a project that uses

Uses Software

• Coq
• Kenzo
• QuickCheck

This page was built for publication: Computing in Coq with infinite algebraic data structures

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