Developing the algebraic hierarchy with type classes in Coq

DOI10.1007/978-3-642-14052-5_35zbMATH Open1291.68370OpenAlexW2152823938MaRDI QIDQ5747673FDOQ5747673

Authors: Bas Spitters, Eelis van der Weegen 

Publication date: 14 September 2010

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_35

Recommendations

• Type classes for mathematics in type theory
• A constructive algebraic hierarchy in Coq.
• Pragmatic quotient types in Coq
• Packaging Mathematical Structures
• Computing in Coq with infinite algebraic data structures

Mathematics Subject Classification ID

Cited In (16)

• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• Formalization of universal algebra in Agda
• Type classes for mathematics in type theory
• Exploring abstract algebra in constructive type theory
• Pragmatic quotient types in Coq
• A constructive algebraic hierarchy in Coq.
• Computing in Coq with infinite algebraic data structures
• Large formal wikis: issues and solutions
• Formalizing implicative algebras in Coq
• Effective homology of bicomplexes, formalized in Coq
• Packaging Mathematical Structures
• Homotopy type theory in Lean
• Working with Mathematical Structures in Type Theory
• Experience implementing a performant category-theory library in Coq
• Category theory in Coq 8.5
• Multiple-inheritance hazards in dependently-typed algebraic hierarchies

Uses Software

• Coq
• C-CoRN

This page was built for publication: Developing the algebraic hierarchy with type classes in Coq

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