Pinned Repositories
CoqEAL
CoqEAL -- The Coq Effective Algebra Library
impro-meta
LaSalle
A formal proof of LaSalle's invariance principle
LFTCM2024_Rocq
Coq/Rocq practice session @ Lean For The Curious Mathematicians 2024
meta-site
Design du site de Meta
coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
analysis
Mathematical Components compliant Analysis Library
finmap
Finite sets, finite maps, multisets and generic sets
math-comp
Mathematical Components
cubicaltt
Experimental implementation of Cubical Type Theory
CohenCyril's Repositories
CohenCyril/LFTCM2024_Rocq
Coq/Rocq practice session @ Lean For The Curious Mathematicians 2024
CohenCyril/lip-ssr-tuto
Ssreflect tutorial for LIP members
CohenCyril/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
CohenCyril/trocq
A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
CohenCyril/addon-mathcomp-extra
More Mathematical Components for jsCoq
CohenCyril/Adjoint
Try to encode in Coq/MathComp the notion of adjoint functor to be able to speak about free monoid / algebra...
CohenCyril/analysis
Mathematical Components compliant Analysis Library
CohenCyril/ceps
Coq Enhancement Proposals
CohenCyril/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.
CohenCyril/Coq-Combi
Algebraic Combinatorics in Coq
CohenCyril/coq-elpi
Coq plugin embedding elpi
CohenCyril/coq-nix-toolbox
Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
CohenCyril/extructures
Finite sets and maps for Coq with extensional equality
CohenCyril/gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
CohenCyril/GeoCoq
A formalization of geometry in Coq based on Tarski's axiom system
CohenCyril/hierarchy-builder
High level commands to declare a hierarchy based on packed classes
CohenCyril/huffman
Correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]
CohenCyril/math-comp
Mathematical Components
CohenCyril/math-comp-nix
Nix support for mathcomp packages
CohenCyril/mathlib4
The math library of Lean 4
CohenCyril/nixpkgs
Nix Packages collection
CohenCyril/platform-docs
A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
CohenCyril/real-closed
Theorems for Real Closed Fields
CohenCyril/reglang
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
CohenCyril/ssprove
A foundational framework for modular cryptographic proofs in Coq
CohenCyril/stablesort
Stable sort algorithms and their stability proofs in Coq
CohenCyril/tarjan
Formalization of Tarjan 72 algorithm in Coq with mathematical components and ssreflect
CohenCyril/templates
Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@palmskog,@Zimmi48]
CohenCyril/trakt
A generic goal preprocessing tool for proof automation tactics in Coq
CohenCyril/vscoq
A Visual Studio Code extension for Coq [maintainers=@rtetley,@maximedenes,@huynhtrankhanh,@thery,@Blaisorblade]