Skip to content
View ejgallego's full-sized avatar

Organizations

@coq @jscoq

Block or report ejgallego

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
15 stars written in Coq
Clear filter

Mathematical Components

Coq 595 117 Updated Dec 21, 2024

Mathematical Components compliant Analysis Library

Coq 211 48 Updated Dec 21, 2024

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

Coq 187 19 Updated Dec 8, 2023

A formalization of geometry in Coq based on Tarski's axiom system

Coq 186 26 Updated May 31, 2024

Formal proof of the Four Color Theorem [maintainer=@ybertot]

Coq 178 22 Updated Nov 15, 2024

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

Coq 129 47 Updated Dec 9, 2024

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]

Coq 112 45 Updated Nov 28, 2024

PeaCoq is a pretty Coq, isn't it?

Coq 106 10 Updated Jul 26, 2021

Monadic effects and equational reasonig in Coq

Coq 71 13 Updated Dec 20, 2024

A Lustre compiler in Coq

Coq 63 6 Updated Nov 22, 2024

Foundational Cryptography Framework for machine-checked proofs of cryptography.

Coq 49 23 Updated Apr 18, 2024

Relation algebra library for Coq

Coq 48 17 Updated Nov 13, 2024

Finite sets, finite maps, multisets and generic sets

Coq 47 28 Updated Dec 20, 2024

Coq plugin for parametricity [maintainer=@proux01]

Coq 45 24 Updated Dec 19, 2024

Class instances for Coq inductive types with little boilerplate

Coq 24 9 Updated Dec 3, 2024