math-comp/real-closed

Theorems for Real Closed Fields

Language: Rocq Prover - Size: 455 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 14 - Forks: 11

math-comp/algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components

Language: Rocq Prover - Size: 365 KB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 35 - Forks: 4

math-comp/odd-order

The formal proof of the Odd Order Theorem

Language: Rocq Prover - Size: 1.74 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 34 - Forks: 16

math-comp/math-comp

Mathematical Components

Language: Rocq Prover - Size: 16.2 MB - Last synced at: 5 days ago - Pushed at: 6 days ago - Stars: 638 - Forks: 124

pi8027/stablesort

Stable sort algorithms and their stability proofs in Rocq

Language: Rocq Prover - Size: 5.26 MB - Last synced at: 1 day ago - Pushed at: 10 days ago - Stars: 25 - Forks: 1

math-comp/multinomials

Multinomials for the Mathematical Components library.

Language: Rocq Prover - Size: 1.37 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 15 - Forks: 13

rocq-community/apery

A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]

Language: Rocq Prover - Size: 304 KB - Last synced at: 10 days ago - Pushed at: 11 days ago - Stars: 25 - Forks: 8

math-comp/mczify

Micromega tactics for Mathematical Components

Language: Rocq Prover - Size: 121 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 25 - Forks: 9

math-comp/cad

Formalizing Cylindrical Algebraic Decomposition related theories in mathcomp

Language: Rocq Prover - Size: 357 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 0 - Forks: 2

math-comp/analysis

Mathematical Components compliant Analysis Library

Language: Rocq Prover - Size: 11.1 MB - Last synced at: 13 days ago - Pushed at: 14 days ago - Stars: 224 - Forks: 59

rocq-community/fav-ssr

Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]

Language: Coq - Size: 351 KB - Last synced at: 16 days ago - Pushed at: 8 months ago - Stars: 49 - Forks: 7

affeldt-aist/monae

Monadic effects and equational reasoning in Rocq

Language: Rocq Prover - Size: 4.83 MB - Last synced at: 17 days ago - Pushed at: about 2 months ago - Stars: 72 - Forks: 14

affeldt-aist/infotheo

A Rocq formalization of information theory and linear error-correcting codes

Language: Rocq Prover - Size: 4.49 MB - Last synced at: 30 days ago - Pushed at: 30 days ago - Stars: 71 - Forks: 17

math-comp/finmap

Finite sets, finite maps, multisets and generic sets

Language: Rocq Prover - Size: 687 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 48 - Forks: 29

math-comp/Abel

A proof of Abel-Ruffini theorem.

Language: Rocq Prover - Size: 397 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 29 - Forks: 8

rocq-community/gaia

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

Language: Rocq Prover - Size: 2.2 MB - Last synced at: about 2 months ago - Pushed at: 2 months ago - Stars: 30 - Forks: 7

rocq-community/fourcolor

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

Language: Coq - Size: 813 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 210 - Forks: 23

rocq-community/reglang

Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]

Language: Coq - Size: 552 KB - Last synced at: 3 months ago - Pushed at: 5 months ago - Stars: 43 - Forks: 7

math-comp/bigenough

Asymptotic reasoning with bigenough

Language: Coq - Size: 26.4 KB - Last synced at: about 2 months ago - Pushed at: 4 months ago - Stars: 4 - Forks: 3

rocq-community/bits

A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]

Language: Coq - Size: 194 KB - Last synced at: about 2 months ago - Pushed at: 4 months ago - Stars: 23 - Forks: 7

rocq-community/autosubst

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

Language: Coq - Size: 913 KB - Last synced at: about 1 month ago - Pushed at: 12 months ago - Stars: 59 - Forks: 15

ilyasergey/pnp

Lecture notes for a short course on proving/programming in Coq via SSReflect.

Language: Coq - Size: 6.47 MB - Last synced at: 4 months ago - Pushed at: about 4 years ago - Stars: 164 - Forks: 19

arthuraa/extructures

Finite sets and maps for Coq with extensional equality

Language: Coq - Size: 489 KB - Last synced at: 2 months ago - Pushed at: 3 months ago - Stars: 30 - Forks: 6

DistributedComponents/disel

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Language: Coq - Size: 1.24 MB - Last synced at: 5 months ago - Pushed at: about 1 year ago - Stars: 98 - Forks: 7

gstew5/games

Language: Coq - Size: 142 KB - Last synced at: 3 days ago - Pushed at: over 5 years ago - Stars: 10 - Forks: 2

rocq-community/tarjan

Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintainers=@CohenCyril,@palmskog]

Language: Coq - Size: 232 KB - Last synced at: 5 months ago - Pushed at: 6 months ago - Stars: 14 - Forks: 8

rocq-community/lemma-overloading

Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]

Language: Coq - Size: 1.1 MB - Last synced at: 2 months ago - Pushed at: 5 months ago - Stars: 27 - Forks: 6

hivert/FormalPowerSeries

Formal power series in mathomp

Language: Coq - Size: 1.44 MB - Last synced at: 2 months ago - Pushed at: 8 months ago - Stars: 3 - Forks: 2

Yosuke-Ito-345/Actuary

Formalization of the basic actuarial mathematics using Coq

Language: Coq - Size: 2.42 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 21 - Forks: 3

anton-trunov/csclub-coq-course-spring-2021

A course on formal verification at https://compsciclub.ru/en, Spring term 2021

Language: HTML - Size: 3.75 MB - Last synced at: 5 months ago - Pushed at: over 2 years ago - Stars: 57 - Forks: 14

rocq-community/regexp-Brzozowski

Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]

Language: Coq - Size: 254 KB - Last synced at: about 2 months ago - Pushed at: about 1 year ago - Stars: 13 - Forks: 1

anton-trunov/ssreflect-mathcomp-talk-moscow-2019

SSReflect/Mathcomp talk at FProg meetup(2019), Moscow

Language: JavaScript - Size: 2.82 MB - Last synced at: 3 months ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 0

anton-trunov/ssreflect-london-tydd-meetup

SSReflect talk at London Type-Driven Development meetup

Language: HTML - Size: 3.17 MB - Last synced at: 5 months ago - Pushed at: over 4 years ago - Stars: 6 - Forks: 1

math-comp/POPLmark

Solutions for the POPLmark challenge

Language: Coq - Size: 38.1 KB - Last synced at: about 2 months ago - Pushed at: almost 6 years ago - Stars: 7 - Forks: 0

proofengineering/regmatch

Certified regular expression matcher in Coq

Language: Coq - Size: 91.8 KB - Last synced at: over 2 years ago - Pushed at: over 5 years ago - Stars: 3 - Forks: 0

palmskog/chip

Change impact analysis in Coq and OCaml

Language: Coq - Size: 353 KB - Last synced at: 5 months ago - Pushed at: almost 4 years ago - Stars: 3 - Forks: 0

CohenCyril/CoqEAL Fork of coq-community/coqeal

CoqEAL -- The Coq Effective Algebra Library

Language: Coq - Size: 1.56 MB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 1 - Forks: 1

CohenCyril/spectral

Spectral Theorem formalized in Coq (Draft)

Language: Coq - Size: 64.5 KB - Last synced at: 5 months ago - Pushed at: about 7 years ago - Stars: 1 - Forks: 1

CohenCyril/signdet

Sign determination for CAD

Language: Coq - Size: 89.8 KB - Last synced at: 5 months ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 1

vyorkin/math-comp-notes

:construction: Repo to keep track of my notes and solutions to the Mathematical components book.

Language: Coq - Size: 14.6 KB - Last synced at: 6 months ago - Pushed at: almost 6 years ago - Stars: 1 - Forks: 0

vyorkin/sf-ssreflect

:construction: Working through the SF using ssreflect

Language: Coq - Size: 15.6 KB - Last synced at: 6 months ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0

esum/internship2019

Language: Coq - Size: 30.3 KB - Last synced at: 2 months ago - Pushed at: about 6 years ago - Stars: 0 - Forks: 0