silene Goto Github PK

aac-tactics

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]

alabaster

Lightweight, configurable Sphinx theme. Now the Sphinx default!

alt-ergo

OCamlPro public development repository for Alt-Ergo

bignums

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

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.

corn

Coq Repository at Nijmegen

interval

lablgtk

Mirror repository for https://forge.ocamlcore.org/anonscm/git/lablgtk/lablgtk.git

metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq

metalibm

Code generation tool to generate mathematical libraries

ocaml

The core OCaml system: compilers, runtime system, base libraries

opam

opam is a source-based package manager. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow.

opam-coq-archive

Archive for all Coq related OPAM packages organized in various repositories

opam-repository

Main public package repository for OPAM, the source package manager of OCaml.

perennial

Verifying concurrent crash-safe systems

pi-agm

A formal description in Coq of computations of PI using arithmetic-geometric means

remake

Remake, a build system that bridges the gap between make and redo

sphinx

Main repository for the Sphinx documentation builder

www-coq

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

zarith

The Zarith library implements arithmetic and logical operations over arbitrary-precision integers and rational numbers. The implementation, based on GMP, is very efficient.