152 Open source projects that are alternatives of or similar to Abel

Finite sets, finite maps, multisets and generic sets

Stable sort algorithms and their stability proofs in Coq

Multinomials for the Mathematical Components library.

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

Formalization of the basic actuarial mathematics using Coq

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

The formal proof of the Odd Order Theorem

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

Formalization of Typed Assembly Language (TAL) in Coq

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

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

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

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

A core language for rule-based hardware design 🦑

A Coq library providing tactics to deal with hypothesis

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

Reference sheet for the Coq language.

Coq plugin embedding elpi

Proof of concept to generate safe and fast JavaScript

Mtac in Agda

A framework for implementing and certifying impure computations in Coq

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

A mechanisation of Wasm in Coq

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

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

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

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

Mutation analysis tool for Coq verification projects

A Learning Environment for Theorem Proving with the Coq proof assistant

No description or website provided.

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

Randomized Property-Based Testing Plugin for Coq

Gallina to Bedrock2 compilation toolkit

Ltac2 tutorial

No description or website provided.

Partial Commutative Monoids

A minimalistic blockchain consensus implemented and verified in Coq

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

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

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

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

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

Goose converts a small subset of Go to Coq

Template project for program verification in Coq

The Vellvm (Verified LLVM) coq development.

Jupyter kernel for Coq

FSCQ is a certified file system written and proven in Coq

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

Metaprogramming in Coq

🐣 A blog engine written and proven in Coq

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

Formalization of the polymorphic lambda calculus and its parametricity theorem

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.

Recipe for FPGA cooking

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

A function definition package for Coq

Formal verification of OCaml programs

Archive for all Coq related OPAM packages organized in various repositories

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT

Convert Haskell source code to Coq source code.