5 results found Sort:

MetaCoq
metacoq MetaCoq
86
430
mit
16
Metaprogramming, verified meta-theory and implementation of Coq in Coq
coq metaprogramming coq-formalization
Created 2017-10-19
4,971 commits to coq-8.20 branch, last one 29 days ago
amintimany
Categories amintimany
4
95
unknown
5
A formalization of category theory in the Coq proof assistant.
coq topos library categories adjunctions kan-extensions category-theory proof-assistant coq-formalization
Created 2015-10-14
160 commits to master branch, last one 4 years ago
bluerock-io
BRiCk bluerock-io
14
75
other
8
Formalization of C++ for verification purposes.
coq cplusplus coq-library cplusplus-11 cplusplus-14 cplusplus-17 cplusplus-20 cplusplus-23 coq-formalization
Created 2020-05-04
5,748 commits to master branch, last one a day ago
INRIA
velus INRIA
6
66
other
9
A Lustre compiler in Coq
lustre compcert coq-formalization synchronous-language
Created 2019-10-21
2,156 commits to paul-thesis branch, last one 2 months ago
SSProve
ssprove SSProve
11
63
mit
8
A foundational framework for modular cryptographic proofs in Coq
coq-library cryptography coq-formalization formal-verification state-separating-proofs modular-cryptographic-proofs
Created 2021-03-09
1,523 commits to main branch, last one about a month ago