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