maximedenes Goto Github PK

aac-tactics

This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators.

bbv

Bedrock Bit Vector Library

bedrock

Not necessarily up-to-date mirror of hg bedrock repository

bedrock2

Towards a low-level systems programming language with a verified compiler

bignums

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

catala

Programming language for literate programming law specification

catala-language-server

color

Coq library on rewriting theory and termination

compcert

The CompCert C verified 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-8.5-demo

coq-amd64

coq-bot

A (Coq Development Team) bot written in OCaml

coq-dpdgraph

Build dependency graphs between COQ objects

coq-elpi

Coq plugin embedding elpi

coq-equations

A plugin for Coq to add dependent pattern-matching.

coq-ext-lib

A library of Coq definitions, theorems, and tactics.

coq-lean-import

coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq

coq-platform

Multi platform setup for Coq, Coq libraries and tools

coq-rst

An experiment in porting Coq's manual to reStructuredText

coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

coq-www

Sources files of the coq.inria.fr website (static part)

coqffi

coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

coqprime

Prime numbers for Coq

coqutil

Coq library for tactics, basic definitions, sets, maps

coqword

Yet Another Coq Library on Machine Words.

corn

Coq Repository at Nijmegen

cross-crypto

Connecting computational and symbolic crypto models