Showing entries 1-83 out of 83.
Coq proof assistant
Language Server Protocol and VS Code Extension for Coq
Coq plugin providing tactics for rewriting universally quantified equations
Exponentiation algorithms following addition chains
Automation for de Bruijn syntax and substitution in Coq
A formalization of category theory in Coq for personal study and practical work
Library for serialization to S-expressions
CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory a…
A formalization of bitset operations in Coq
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
The CoqIDE user interface for the Coq proof assistant
Library to certify primality using Pocklington certificate and Elliptic Curve Certificate
A Coq library for Reals
A Coq library for constructive analysis
Generic instances of MathComp classes
Build dependency graphs between Coq objects
Coq plugin embedding ELPI
A plugin for Coq to add dependent pattern-matching
Finite data structures with extensional reasoning
A 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
Comparison between ordinals in Gaia and Hydra battles
Coq support library for Gappa
The Gödel-Rosser 1st incompleteness theorem in Coq
Library of formalized graph theory results in Coq
High level commands to declare a hierarchy based on packed classes
Homotopy type theory
Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq
A Library for Representing Recursive and Impure Programs in Coq
Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proo…
The Coq development of the Iris Project
A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support
Hypotheses manipulation library
A library of abstract interfaces for mathematical structures in Coq
Abel - Galois and Abel - Ruffini Theorems
Ring and field tactics for Mathematical Components
A small library to do epsilon - N reasonning
A finset and finmap library
Analysis library compatible with Mathematical Components
Analysis library compatible with Mathematical Components
A 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
Formal proof of the Odd Order Theorem
A Coq library implementing parameterized coinduction
Coq plugin for parametricity
Library for serialization to S-expressions
Pocklington's criterion for primality in Coq
Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck
Regular Language Representations in Coq
Relation algebra library for Coq
A survey of programming language semantics styles in Coq
SerAPI is a library for machine-to-machine interaction with the Coq proof assistant
Purely functional IO for Coq
An extended “Standard Library” for Coq
A non-constructive library for Coq
General topology in Coq
A generic goal preprocessing tool for proof automation tactics in Coq
Verified Software Toolchain
Development of basic set theory