Showing entries 1-60 out of 60.
Coq proof assistant
Automation for de Bruijn syntax and substitution in Coq
Library for serialization to S-expressions
CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory a…
Collection of theories and plugins that may be useful in other Coq developments
Library to create Coq record update functions
CoqEAL - The Coq Effective Algebra Library
Coq library for Reals
Generic instances of MathComp classes
Coq plugin embedding ELPI
Plugin for Coq to add dependent pattern-matching
Finite data structures with extensional reasoning
Floating-point formalization for the Coq system
Formal proof of the Four Color Theorem
Implementation of books from Bourbaki's Elements of Mathematics in Coq
High level commands to declare a hierarchy based on packed classes
Library for Representing Recursive and Impure Programs in Coq
Coq development of the Iris Project
Jasmin language & verified compiler
From JSON to Coq, and vice versa
Ring and field tactics for Mathematical Components
Small library to do epsilon - N reasonning
Finset and finmap library
Coq/SSReflect Library for Monoidal Rings and Multinomials
Mathematical Components Library on real closed fields
Proofs of Tarjan and Kosaraju connected components algorithms
Yet Another Coq Library on Machine Words
Micromega tactics for Mathematical Components
A support library for verified Coq parsers produced by Menhir
Formal proof of the Odd Order Theorem
Coq library implementing parameterized coinduction
Library for serialization to S-expressions
Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck
Regular Language Representations in Coq
Purely functional IO for Coq
Compatibility metapackage for Coq Stdlib library after the Rocq renaming
Extended “Standard Library” for Coq