ybertot Goto Github PK

analysis

Mathematical Components compliant Analysis Library

awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]

breadth_first_search

A generic algorithm for breadth first search, in Coq, with proofs

cad

Formalizing Cylindrical Algebraic Decomposition related theories in mathcomp

cbench

A benchmark for C program verification

cbench-vst

VST verification of programs from the cbench benchmark

checker

an attempt at making a toy proof checker for experimental purposes

coind_filters

Coq code associated to an article published at TLCA'05 "Filters on Co-inductive Streams..."

coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

coq-art

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

coq-dpdgraph

Build dependency graphs between COQ objects

coq-elpi

Coq plugin embedding elpi

coq-equations

A function definition package for Coq

coq-function-equations

A case study on using Function and Equations to avoid case explosion in proofs about pattern-matching

coq-lsp

Language Server Protocol and VS Code Extension for Coq

coqeal

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

cws16

coq winter school 2016

exact-real-arithmetic

Exact Real Arithmetic [maintainers=@ybertot,@magaud]

extructures

Finite sets and maps for Coq with extensional equality

finmap

Finset and finmap library

formal-proofs-for-the-convergence-of-visibility-walks-in-triangulations

fourcolor

Formal proof of the Four Color Theorem

fset_exercises

Didactic material for Coq

fsets

Finite Sets overs Ordered Types

hierarchy-builder

High level commands to declare a hierarchy based on packed classes

highschoolgeometry

Geometry in Coq for French high school [maintainer=@thery]

hinitiality

hott

Homotopy type theory

hulls

Hulls

hydra-battles

Variations on Kirby & Paris' hydra battles and other funny maths (collaborative, documented, include exercises) [maintainer=@Casteran]