math-classes

Math library

A library of abstract interfaces for various mathematical structures to facilitate algebraic manipulation and type class-based reasoning in Coq

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

GitHub

162 stars
16 watching
43 forks
Language: Coq
last commit: almost 2 years ago
Linked from 2 awesome lists

coqcoq-cicoq-librarycoq-platformmathematicstypeclasses

Backlinks from these awesome lists:

Related projects:

RepositoryDescriptionStars
coq-community/coqealA Coq library providing algebraic data structures and algorithms67
coq-community/cornA comprehensive formalization of mathematical structures and concepts for verified computation in Coq.111
charguer/tlcA Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems.38
coq-community/gaiaA Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics30
coq-community/coqtail-mathA collection of mathematical theorems and tools within the Coq proof assistant15
coq-community/topologyDevelops and formalizes basic concepts and results of general topology in Coq.47
math-comp/math-compA comprehensive library of formalized mathematical theories593
coq-community/parsequeA Coq library that provides a total parser combinator library with support for building parsers and grammars in the language of Coq.42
coq-community/graph-theoryFormalized graph theory results for research and verification35
math-comp/analysisA Coq proof-assistant library for real analysis and mathematical structures210
coq-community/bignumsA Coq library providing support for arbitrarily large numbers22
coq-community/reglangProvides definitions and verified translations between various representations of regular languages in the Coq proof assistant41
coq-community/coq-ext-libA collection of reusable Coq definitions and theorems for building software development tools129
coq-community/semanticsA comprehensive survey of programming language semantics styles implemented in Coq46
coq-community/atbrA Coq library providing algebraic tools and tactics for working with binary relations23