hierarchy-builder

Hierarchy builder

Provides high-level commands to declare hierarchical algebraic structures in Coq using packed classes

High level commands to declare a hierarchy based on packed classes

GitHub

97 stars
18 watching
22 forks
Language: Prolog
last commit: about 1 month ago
Linked from 2 awesome lists

coqelpimathcomp

Backlinks from these awesome lists:

Related projects:

Repository Description Stars
philzook58/nand2coq An educational project building a formally verified version of the Nand 2 Tetris course using Coq and other formal tools. 54
math-comp/math-comp A comprehensive library of formalized mathematical theories 593
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
math-comp/coq-combi Formalizes algebraic combinatorics and symmetric functions in Coq. 37
coq-community/coqeal A Coq library providing algebraic data structures and algorithms 67
coq-community/gaia A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics 30
pa-ba/calc-comp Formalizations of compiler design and virtual machine calculations in Coq 30
closuretree/closure_tree A Ruby library for building hierarchical data models in ActiveRecord 1,848
cristalhq/builq A simple and safe Go library for building SQL queries with parameter indexing. 91
thery/mathcomp-extra A collection of reusable mathematical components and algorithms implemented in Coq 5
math-comp/analysis A Coq proof-assistant library for real analysis and mathematical structures 210
charguer/tlc A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. 38
coq-community/lemma-overloading A Coq library demonstrating design patterns for automated proof automation and canonical structures 26
coq-community/hydra-battles Investigating various aspects of discrete mathematics and formal proofs in Coq, including ordinal numbers and computability theory. 69