160 Open source projects that are alternatives of or similar to multinomials

Finite sets, finite maps, multisets and generic sets

The formal proof of the Odd Order Theorem

A proof of Abel-Ruffini theorem.

Stable sort algorithms and their stability proofs in Coq

Formalization of the basic actuarial mathematics using Coq

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

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

A core language for rule-based hardware design 🦑

A library of mechanised undecidability proofs in the Coq proof assistant.

No description or website provided.

Formalization of Typed Assembly Language (TAL) in Coq

A formally verified high-level synthesis tool based on CompCert and written in Coq.

Advanced Combinatorics and Algebraic Number Theory Symbolic Computation library for JavaScript, Python

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.

Template project for program verification in Coq

A minimalistic blockchain consensus implemented and verified in Coq

Statements of famous theorems proven in Coq [maintainer=@jmadiot]

A Julia package to handle spherical harmonic functions

A framework for implementing and certifying impure computations in Coq

Mutation analysis tool for Coq verification projects

Intermediate Memory Model (IMM) and compilation correctness proofs for it

A mechanisation of Wasm in Coq

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

Formalization of the polymorphic lambda calculus and its parametricity theorem

The Vellvm (Verified LLVM) coq development.

FSCQ is a certified file system written and proven in Coq

A JuMP extension for Polynomial Optimization

Gallina to Bedrock2 compilation toolkit

Archive for all Coq related OPAM packages organized in various repositories

Metaprogramming in Coq

No description or website provided.

Coq to OCaml FFI made easy [maintainer=@lthms]

A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

Reference sheet for the Coq language.

C++ special math functions

Coq plugin embedding elpi

Proof of concept to generate safe and fast JavaScript

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

We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

A Coq library providing tactics to deal with hypothesis

Goose converts a small subset of Go to Coq

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

equadratures.org/

Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on

Voevodsky's original development of the univalent foundations of mathematics in Coq

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

A Learning Environment for Theorem Proving with the Coq proof assistant

Sum of Squares Programming for Julia

Convert Haskell source code to Coq source code.

Randomized Property-Based Testing Plugin for Coq

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

🐣 A blog engine written and proven in Coq

Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]

Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]

Recipe for FPGA cooking

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

A function definition package for Coq

Givaro - C++ library for arithmetic and algebraic computations