Showing entries 1-53 out of 53.
Language Server Protocol and VS Code Extension for Coq
Formally verified C compiler
Coq plugin providing tactics for rewriting universally quantified equations
Coq library and tactic for deciding Kleene algebras
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
CoqIDE user interface for the Coq proof assistant
Library to certify primality using Pocklington certificate and Elliptic Curve Certificate
Coq library for Reals
Coq library for constructive analysis
Generic instances of MathComp classes
A framework for extracting Coq programs to Elm
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
Coq support library for Gappa
High level commands to declare a hierarchy based on packed classes
Geometry in Coq for French high school
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…
Reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support
From JSON to Coq, and vice versa
Hypotheses manipulation library
Library of abstract interfaces for mathematical structures in Coq
Ring and field tactics for Mathematical Components
Small library to do epsilon - N reasonning
Finset and finmap library
Analysis library compatible with Mathematical Components
Analysis library compatible with Mathematical Components
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
Coq library implementing parameterized coinduction
Coq plugin for parametricity
Library for serialization to S-expressions
Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck
Regular Language Representations in Coq
SerAPI is a library for machine-to-machine interaction with the Coq proof assistant
Purely functional IO for Coq
A two-level approach to prove tautologies using Stålmarck's algorithm in Coq
Coq tactic and verified tool for proving tautologies using Stålmarck's algorithm
Development of basic set theory
Language server for the vscoq vscode/codium extension