Developing the algebraic hierarchy with type classes in Coq

DOI10.1007/978-3-642-14052-5_35MaRDI QIDQ5747673zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Describes a project that uses

Uses Software

• C-CoRN
• Coq

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)