Coq-Equations
Function definition plugin
A package for defining functions in Coq using dependent types and pattern-matching.
A function definition package for Coq
223 stars
10 watching
45 forks
Language: Coq
last commit: 3 months ago
Linked from 2 awesome lists
coqdependent-typesprogramming-language
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 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 |
| coq-community/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 45 |
 math-comp/tutorial_material | Tutorials and materials for teaching Coq-based mathematical component development | 17 |
| coq-community/parseque | A Coq library that provides a total parser combinator library with support for building parsers and grammars in the language of Coq. | 42 |
 coq-io/io | A Coq library that enables the use of effects in functional programming with references to a global state | 64 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 30 |
| coq-community/aac-tactics | Tactics for rewriting and proving equations with associativity and commutativity properties | 29 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 168 |
 samuelgruetter/dot-calculus | A formalization of Dependent Object Types (DOT) calculus in Coq to support type safety proofs for a new foundation for Scala's type system | 62 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |
| coq-io/system | A library of Unix effects implemented in the Coq functional programming language | 23 |
| math-comp/analysis | A Coq proof-assistant library for real analysis and mathematical structures | 210 |
 llee454/functional-algebra | A Coq formalization of abstract algebra using functional programming style | 28 |