functional-algebra
Algebra library
A Coq formalization of abstract algebra using functional programming style
This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.
28 stars
1 watching
2 forks
Language: Coq
last commit: over 5 years ago certified-programmingcoqcoq-formalizationcoq-librarymathematicstheorem-proving
Related projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 66 |
 discus-lang/iron | Formalizations of functional languages with a focus on proof and verification | 141 |
| coq-community/atbr | A Coq library providing algebraic tools and tactics for working with binary relations | 23 |
 vafeiadis/hahn | A collection of lemmas and tactics about lists and binary relations for a proof assistant | 30 |
 math-comp/coq-combi | Formalises algebraic combinatorics in Coq using symmetric functions and polynomials | 36 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
| math-comp/abel | Formalization of mathematical theorems about solvability and Galois theory for polynomials | 28 |
| coq-community/math-classes | A library of abstract interfaces for various mathematical structures to facilitate algebraic manipulation and type class-based reasoning in Coq | 162 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 arthuraa/extructures | Provides data structures and reasoning tools for extensional equality in Coq | 29 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 28 |
 geocoq/geocoq | A formalization of geometry using the Coq proof assistant. | 186 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |