GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → coq-community → gaia

coq-community / gaia

Licence: MIT License
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

Programming Languages

Coq
218 projects

Labels

coqset-theoryssreflectmathcompdocker-coq-actionbourbaki

Projects that are alternatives of or similar to gaia

odd-order
The formal proof of the Odd Order Theorem
Stars: ✭ 20 (+33.33%)
Mutual labels:  coq, ssreflect, mathcomp
Abel
A proof of Abel-Ruffini theorem.
Stars: ✭ 26 (+73.33%)
Mutual labels:  coq, ssreflect, mathcomp
autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
Stars: ✭ 41 (+173.33%)
Mutual labels:  coq, ssreflect, mathcomp
finmap
Finite sets, finite maps, multisets and generic sets
Stars: ✭ 45 (+200%)
Mutual labels:  coq, ssreflect, mathcomp
stablesort
Stable sort algorithms and their stability proofs in Coq
Stars: ✭ 19 (+26.67%)
Mutual labels:  coq, ssreflect, mathcomp
Actuary
Formalization of the basic actuarial mathematics using Coq
Stars: ✭ 17 (+13.33%)
Mutual labels:  coq, ssreflect, mathcomp
multinomials
Multinomials for the Mathematical Components library.
Stars: ✭ 12 (-20%)
Mutual labels:  coq, ssreflect, mathcomp
coq-art
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Stars: ✭ 57 (+280%)
Mutual labels:  coq, docker-coq-action
chapar
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
Stars: ✭ 29 (+93.33%)
Mutual labels:  coq, docker-coq-action
bignums
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
Stars: ✭ 20 (+33.33%)
Mutual labels:  coq, docker-coq-action
Set-Theory
Coq encoding of ZFC and formalization of the textbook Elements of Set Theory
Stars: ✭ 55 (+266.67%)
Mutual labels:  coq, set-theory
coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Stars: ✭ 62 (+313.33%)
Mutual labels:  coq, mathcomp
hydra-battles
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
Stars: ✭ 38 (+153.33%)
Mutual labels:  coq, docker-coq-action
coq-big-o
A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
Stars: ✭ 31 (+106.67%)
Mutual labels:  coq
RiscvSpecFormal
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
Stars: ✭ 69 (+360%)
Mutual labels:  coq
coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
Stars: ✭ 84 (+460%)
Mutual labels:  coq
activerecord-setops
Union, Intersect, and Difference set operations for ActiveRecord (also, SQL's UnionAll).
Stars: ✭ 21 (+40%)
Mutual labels:  set-theory
coq-program-verification-template
Template project for program verification in Coq
Stars: ✭ 26 (+73.33%)
Mutual labels:  coq
imm
Intermediate Memory Model (IMM) and compilation correctness proofs for it
Stars: ✭ 15 (+0%)
Mutual labels:  coq
FreeSpec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 48 (+220%)
Mutual labels:  coq
View All Similar Projects ➔

Gaia

Docker CI Contributing Code of Conduct Zulip

Implementation of books from N. Bourbaki's Elements of Mathematics in Coq using the Mathematical Components library, including set theory and number theory.

Meta

Building and installation

To build and install manually, do:

git clone https://github.com/coq-community/gaia.git
cd gaia
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

Gaia stands for: Geometry, Algebra, Informatics and Applications. More information about the project is available at the project website.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].