vbgl

Pinned Repositories

aac-tactics
This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainers=@fakusb,@palmskog]
Language:OCaml0 1 00
apron
Apron Numerical Abstract Domain Library
Language:C0 1 00
batteries-included
Batteries Included project
Language:OCaml0 1 00
bignums
Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
Language:Coq0 2 00
comby
A code rewrite tool for structural search and replace that supports ~every language.
Language:OCaml0 0 00
CompCert
The CompCert formally-verified C compiler
Language:Coq0 2 00
containers
Containers: a typeclass-based library of finite sets/maps
Language:Coq0 2 00
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.
Language:OCaml0 2 00

vbgl's Repositories

vbgl/nixpkgs
Nix Packages collection
Language:Nix1 3 00
vbgl/aac-tactics
This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainers=@fakusb,@palmskog]
Language:OCaml0 1 00
vbgl/apron
Apron Numerical Abstract Domain Library
Language:C0 1 00
vbgl/batteries-included
Batteries Included project
Language:OCaml0 1 00
vbgl/bignums
Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
Language:Coq0 2 00
vbgl/comby
A code rewrite tool for structural search and replace that supports ~every language.
Language:OCaml0 0 00
vbgl/CompCert
The CompCert formally-verified C compiler
Language:Coq0 2 00
vbgl/containers
Containers: a typeclass-based library of finite sets/maps
Language:Coq0 2 00
vbgl/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.
Language:OCaml0 2 00
vbgl/coq-dpdgraph
Build dependency graphs between COQ objects
Language:Coq2 0
vbgl/coq-nix-toolbox
Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
Language:Nix1 0
vbgl/cross-crypto
Connecting computational and symbolic crypto models
Language:Coq2 0
vbgl/dead_code_analyzer
Dead-code analyzer for OCaml
Language:OCaml1 0
vbgl/easycrypt
EasyCrypt: Computer-Aided Cryptographic Proofs
Language:OCaml2 0
vbgl/ExactPredicates.jl
Fast and exact geometrical predicates in the Euclidean plane
Language:Julia
vbgl/formosa-keccak
Implementation of Keccak and related functions (SHA3, SHAKE, etc.)
vbgl/hakyber
Language:eC1 0
vbgl/implementation-ladder
A set of examples of crypto implementations
vbgl/jasmin-doc
Language:Python0 0
vbgl/liquidsoap
Liquidsoap is a statically typed scripting general-purpose language with dedicated operators and backend for all thing media, streaming, file generation, automation, HTTP backend and more.
Language:OCaml1 0
vbgl/mathcomp-word
Yet Another Coq Library on Machine Words.
Language:Coq0 0
vbgl/Obelisk
A simple multi-format pretty-printer for Menhir.
Language:OCaml1 0
vbgl/ocsigen-start
Ocsigen-start: Higher-level library to develop Web and mobile applications with users, (pre)registration, notifications, etc.
vbgl/ocsigenserver
Web server in OCaml.
vbgl/Pluto.jl
🎈 Simple reactive notebooks for Julia
Language:Julia0 0
vbgl/scverif
Language:OCaml0 0
vbgl/sdcc
Small Device C Compiler
Language:C0 0
vbgl/sile-typesetter.github.io
Github Pages source code for https://sile-typesetter.org
Language:HTML1 0
vbgl/VplTactic
A Coq Tactic for Arithmetic (based on VPL)
Language:Coq1 0
vbgl/VST
Verified Software Toolchain
Language:Coq2 0