All Projects → coq-community → bignums

coq-community / bignums

Licence: LGPL-2.1 license
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

Programming Languages

Coq
218 projects
ocaml
1615 projects
Makefile
30231 projects

Projects that are alternatives of or similar to bignums

PUMPKIN-PATCH
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
Stars: ✭ 43 (+115%)
Mutual labels:  coq, coq-plugin
coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Stars: ✭ 62 (+210%)
Mutual labels:  coq, coq-platform
gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Stars: ✭ 15 (-25%)
Mutual labels:  coq, docker-coq-action
hydra-battles
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
Stars: ✭ 38 (+90%)
Mutual labels:  coq, docker-coq-action
coq-art
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Stars: ✭ 57 (+185%)
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 (+45%)
Mutual labels:  coq, docker-coq-action
corn
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]
Stars: ✭ 106 (+430%)
Mutual labels:  coq, coq-platform
toychain
A minimalistic blockchain consensus implemented and verified in Coq
Stars: ✭ 103 (+415%)
Mutual labels:  coq
Actuary
Formalization of the basic actuarial mathematics using Coq
Stars: ✭ 17 (-15%)
Mutual labels:  coq
coq-100-theorems
Statements of famous theorems proven in Coq [maintainer=@jmadiot]
Stars: ✭ 41 (+105%)
Mutual labels:  coq
opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
Stars: ✭ 101 (+405%)
Mutual labels:  coq
coq-tal
Formalization of Typed Assembly Language (TAL) in Coq
Stars: ✭ 15 (-25%)
Mutual labels:  coq
iris-simp-lang
We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.
Stars: ✭ 40 (+100%)
Mutual labels:  coq
CoqCheatSheet
Reference sheet for the Coq language.
Stars: ✭ 15 (-25%)
Mutual labels:  coq
coq-elpi
Coq plugin embedding elpi
Stars: ✭ 92 (+360%)
Mutual labels:  coq
coq-to-ocaml-to-js
Proof of concept to generate safe and fast JavaScript
Stars: ✭ 25 (+25%)
Mutual labels:  coq
koika
A core language for rule-based hardware design 🦑
Stars: ✭ 103 (+415%)
Mutual labels:  coq
hs-to-coq
Convert Haskell source code to Coq source code.
Stars: ✭ 64 (+220%)
Mutual labels:  coq
coqffi
Coq to OCaml FFI made easy [maintainer=@lthms]
Stars: ✭ 27 (+35%)
Mutual labels:  coq
stablesort
Stable sort algorithms and their stability proofs in Coq
Stars: ✭ 19 (-5%)
Mutual labels:  coq

Bignums

Docker CI Contributing Code of Conduct Zulip

This Coq library provides BigN, BigZ, and BigQ that used to be part of the standard library.

Meta

  • Author(s):
    • Laurent Théry
    • Benjamin Grégoire
    • Arnaud Spiwack
    • Evgeny Makarov
    • Pierre Letouzey
  • Coq-community maintainer(s):
  • License: GNU Lesser General Public License v2.1
  • Compatible Coq versions: master (use the corresponding branch or release for other Coq versions)
  • Compatible OCaml versions: all versions supported by Coq
  • Additional dependencies: none
  • Coq namespace: Bignums
  • Related publication(s): none

Building and installation instructions

The easiest way to install the latest released version of Bignums is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-bignums

To instead build and install manually, do:

git clone https://github.com/coq-community/bignums.git
cd bignums
make   # or make -j <number-of-cores-on-your-machine> 
make install
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].