villetaneuse Goto Github PK

autosubst

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

bbv

Bedrock Bit Vector Library

bedrock2

A work-in-progress language and compiler for verified low-level programming

ceps

Coq Enhancement Proposals

color

Coq library on rewriting theory and termination

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-art

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

coq-dpdgraph

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

coq-equations

A function definition package for Coq

coq-ext-lib

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

coq-scripts

Various useful scripts for dealing with Coq files

coqprime

Prime numbers for Coq

coqswitch

Help switching between Coq development environments

corn

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

cross-crypto

Connecting computational and symbolic crypto models

fcf

Foundational Cryptography Framework for machine-checked proofs of cryptography.

fiat

Mostly Automated Synthesis of Correct-by-Construction Programs

fiat-crypto

Cryptographic Primitive Code Generation by Fiat

interactiontrees

A Library for Representing Recursive and Impure Programs in Coq

jscoq

A port of Coq to Javascript -- Run Coq in your Browser

kami

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]

metacoq

Metaprogramming in Coq

mtac2

perennial

Verifying concurrent crash-safe systems

platform-docs

A project of short tutorials and how-to guides for Coq features and Coq Platform packages.

quickchick

Randomized Property-Based Testing Plugin for Coq

rewriter

Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting

rupicola

Gallina to Bedrock2 compilation toolkit

sf