Pinned Repositories
aac-tactics
This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainers=@fakusb,@palmskog]
apron
Apron Numerical Abstract Domain Library
batteries-included
Batteries Included project
bignums
Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
comby
A code rewrite tool for structural search and replace that supports ~every language.
CompCert
The CompCert formally-verified C compiler
containers
Containers: a typeclass-based library of finite sets/maps
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.
vbgl's Repositories
vbgl/pigmentoj
Modules for Pygments
vbgl/HoTT
Homotopy type theory
vbgl/kittel-koat
KITTeL/KoAT
vbgl/lablgtk
LablGTK 2 and 3: an interface to the GIMP Tool Kit
vbgl/lablgtk3
vbgl/lsplib
vbgl/ltac2
A standalone implementation of Ltac2 as a Coq plugin
vbgl/math-comp
Mathematical Components
vbgl/Mtac2
vbgl/patoline
Patoline typesetting system
vbgl/reason-gl-matrix
Cross-platform high-performance vector and matrix math for OpenGL
vbgl/stdlib2
vbgl/vbgl.github.io
Source files of the coq.inria.fr website (static part)
vbgl/yamlpp
A very simple HTML preprocessor
vbgl/Zarith
The Zarith library implements arithmetic and logical operations over arbitrary-precision integers and rational numbers. The implementation, based on GMP, is very efficient.