Pinned Repositories
autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
bbv
Bedrock Bit Vector Library
bedrock2
A work-in-progress language and compiler for verified low-level programming
ceps
Coq Enhancement Proposals
color
Coq library on rewriting theory and termination
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-art
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
coqlibdiff
Small scripts to examine user visible changes in a Coq library
coqswitch
Help switching between Coq development environments
platform-docs
A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
Villetaneuse's Repositories
Villetaneuse/autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
Villetaneuse/bbv
Bedrock Bit Vector Library
Villetaneuse/bedrock2
A work-in-progress language and compiler for verified low-level programming
Villetaneuse/color
Coq library on rewriting theory and termination
Villetaneuse/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.
Villetaneuse/coqlibdiff
Small scripts to examine user visible changes in a Coq library
Villetaneuse/coqswitch
Help switching between Coq development environments
Villetaneuse/platform-docs
A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
Villetaneuse/coq-dpdgraph
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
Villetaneuse/Coq-Equations
A function definition package for Coq
Villetaneuse/coq-ext-lib
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
Villetaneuse/coq-scripts
Various useful scripts for dealing with Coq files
Villetaneuse/corn
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]
Villetaneuse/cross-crypto
Connecting computational and symbolic crypto models
Villetaneuse/fcf
Foundational Cryptography Framework for machine-checked proofs of cryptography.
Villetaneuse/fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
Villetaneuse/fiat-crypto
Cryptographic Primitive Code Generation by Fiat
Villetaneuse/InteractionTrees
A Library for Representing Recursive and Impure Programs in Coq
Villetaneuse/ipf-2023
Initiation aux preuves formelles 2023
Villetaneuse/jscoq
A port of Coq to Javascript -- Run Coq in your Browser
Villetaneuse/kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Villetaneuse/math-classes
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]
Villetaneuse/metacoq
Metaprogramming in Coq
Villetaneuse/Mtac2
Villetaneuse/perennial
Verifying concurrent crash-safe systems
Villetaneuse/QuickChick
Randomized Property-Based Testing Plugin for Coq
Villetaneuse/rewriter
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Villetaneuse/rupicola
Gallina to Bedrock2 compilation toolkit
Villetaneuse/sf
Villetaneuse/smtcoq
Communication between Coq and SAT/SMT solvers