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

(17)

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

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)