mrhaandi Goto Github PK

analysis

Mathematical Components compliant Analysis Library

bbv

Bedrock Bit Vector Library

bedrock2

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

bignums

Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library

cls-fsharp

Implementation of the Combinatory Logic Synthesizer algorithm in F#

color

Coq library on rewriting theory and termination

compcert

The CompCert formally-verified C compiler

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-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-library-undecidability

A library of formalised undecidable problems in Coq

coqprime

Prime numbers for Coq

coqutil

Coq library for tactics, basic definitions, sets, maps

corn

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

cross-crypto

Connecting computational and symbolic crypto models

engine-bench

Benchmarks for various proof engines

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

flocq

geocoq

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

ipc2

Reduction from Diophantine equations to provability in IPC2 / System F.

kami

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

lambda-cap

Reduction from simple semi-Thue system rewriting to inhabitation in the Coppo-Dezani type assignment system.

math-classes

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

metacoq

Metaprogramming in Coq

mtac2

paramcoq

Coq plugin for parametricity [maintainer=@proux01]

perennial

Verifying concurrent crash-safe systems