Lists (30)
agda
1 repository
autodiff
4 repositories
c/c++
3 repositories
compiler
67 repositories
cpp
1 repository
cuda
4 repositories
diffusion
1 repository
dynamic
13 repositories
elisp
1 repository
emacs
1 repository
fortran
7 repositories
functional_python
4 repositories
futhark
4 repositories
generative_model
2 repositories
haskell_utils
38 repositories
juliaTensors
3 repositories
lang
52 repositories
llm
3 repositories
MCMC
35 repositories
MD
molecular dynamic7 repositories
numeric
8 repositories
ocaml
2 repositories
optimizer
6 repositories
protein&matter
61 repositories
qc_formal_verification
1 repository
quantum computing
74 repositories
rl
3 repositories
statistics
6 repositories
symbolic
8 repositories
theorem_prove
3 repositories
Starred repositories
13
stars
written in Coq
Clear filter
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Metaprogramming, verified meta-theory and implementation of Coq in Coq
Mathematical Components compliant Analysis Library
A framework for smart contract verification in Coq
A quantum circuit language and formal verification tool
Coq library for reasoning about quantum programs
Proof Object Transformation, Preserving Imp Embeddings: the first proof compiler to be formally proven correct
Extracting Futhark code from the Coq proof assistant
Formal proof of STLC type soundness (progress and preservation) using Coq.
