Pinned Repositories
breadth_first_search
A generic algorithm for breadth first search, in Coq, with proofs
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-dpdgraph
Build dependency graphs between COQ objects
HoTT
Homotopy type theory
math-comp
Mathematical Components
mcb
Mathematical Components (the Book)
opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
plugin_tutorials
A collection of small projects to illustrate how to write plugins for Coq
practical-fm
A gently curated list of companies using verification formal methods in industry
ybertot's Repositories
ybertot/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
ybertot/breadth_first_search
A generic algorithm for breadth first search, in Coq, with proofs
ybertot/coq-dpdgraph
Build dependency graphs between COQ objects
ybertot/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.
ybertot/math-comp
Mathematical Components
ybertot/mcb
Mathematical Components (the Book)
ybertot/reachout_math
internship on making more easily accessible formalized mathematics using Coq
ybertot/analysis
Mathematical Components compliant Analysis Library
ybertot/awesome-coq
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]
ybertot/cbench
A benchmark for C program verification
ybertot/coq-art
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
ybertot/coq-elpi
Coq plugin embedding elpi
ybertot/coq-lsp
Language Server Protocol and VS Code Extension for Coq
ybertot/coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
ybertot/extructures
Finite sets and maps for Coq with extensional equality
ybertot/Formal-proofs-for-the-convergence-of-visibility-walks-in-triangulations
ybertot/fourcolor
Formal proof of the Four Color Theorem
ybertot/hierarchy-builder
High level commands to declare a hierarchy based on packed classes
ybertot/itp-conference.github.io
ybertot/math-comp-nix
Nix support for mathcomp packages
ybertot/one_num_type
ybertot/osxp_demos_coq
ybertot/pi-agm
A formal description in Coq of computations of PI using arithmetic-geometric means
ybertot/platform
Multi platform setup for Coq, Coq libraries and tools
ybertot/real-closed
Theorems for Real Closed Fields
ybertot/semantics
A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
ybertot/trajectories
ybertot/VerticalCells
ybertot/voronoi-fortune
Fortune's algorithm described in coq
ybertot/www
Sources files of the coq.inria.fr website (static part)