ssreflect 开源项目推荐（41 个）

math-comp /math-comp

数学组成部分

rocq-community /fourcolor

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

math-comp /analysis

Mathematical Components compliant Analysis Library

ilyasergey /pnp

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

DistributedComponents /disel

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

rocq-community /autosubst

de Bruijn语法的自动化和Coq中的替换[maintainers=@RalfJung，@co-dan]

affeldt-aist /monae

Monadic effects and equational reasoning in Rocq

affeldt-aist /infotheo

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

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

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

math-comp /finmap

Finite sets, finite maps, multisets and generic sets

rocq-community /fav-ssr

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

rocq-community /reglang

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

math-comp /odd-order

The formal proof of the Odd Order Theorem

math-comp /mczify

Micromega tactics for Mathematical Components

arthuraa /extructures

Finite sets and maps for Coq with extensional equality

math-comp /Abel

A proof of Abel-Ruffini theorem.

rocq-community /gaia

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

rocq-community /lemma-overloading

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

pi8027 /stablesort

Stable sort algorithms and their stability proofs in Rocq

rocq-community /apery

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