coq-formalization
There are 91 repositories under coq-formalization topic.
MetaCoq/metacoq
Metaprogramming, verified meta-theory and implementation of Coq in Coq
verse-lab/ceramist
Verified hash-based AMQ structures in Coq
amintimany/Categories
A formalization of category theory in the Coq proof assistant.
bluerock-io/BRiCk
Formalization of C++ for verification purposes.
INRIA/velus
A Lustre compiler in Coq
SSProve/ssprove
A foundational framework for modular cryptographic proofs in Coq
sigurdschneider/lvc
LVC verified compiler
Blaisorblade/dot-iris
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
llee454/functional-algebra
This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.
verif-scop/PolCert
A verified polyhedral scheduling validator in Coq.
VERIMAG-Polyhedra/VPL
Verimag Polyhedra Library
thery/grobner
A fornalisation of Grobner basis in ssreflect
uds-psl/CoqTM
Formalising Turing Machines In Coq (bachelor's thesis)
Mbodin/CoqR
A Coq formalisation of the R programming language
acorrenson/automatik
A library of formalized automaton algorithms
PnVDiscord/PnVRocqLib
A Coq library written by members of PnV Discord Server
bor0/formal-ed
Paper: Formalizing line editors in Coq
thery/lemonde
les problèmes proposés par le journal Le Monde en Coq
yiyunliu/mltt-consistency
Logical relation for predicative CC omega with booleans and an intensional identity type
lukaszcz/COQ-IMP
Coq version of (part of) the HOL-IMP theories accompanying the book "Concrete Semantics with Isabelle/HOL". Formalized using a now outdated version of CoqHammer.
TheoWinterhalter/ett-to-wtt
Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory
thery/Plouffe
Computing Pi decimal using Plouffe Formula in Coq
jgrosso/coq-alpha-pearl
Coq formalization of "Functional Pearls: α-conversion is easy" (Altenkirch, 2002).
cogumbreiro/habanero-coq
Coq formalization of the Habanero programming model.
DmxLarchey/Coq-is-total
A proof that Coq contains any total mu-recursive function
Kamirus/lambda-formalizations
Lambda Calculi Formalizations in Coq using nested datatypes for a type-safe term representation
thery/twoSquare
A proof of Fermat's theorem on sum of two squares with mathcom using gaussian integers.
wkolowski/CoqCat
Formalization of Category Theory in Coq.
ComFreek/basic-ontology-language
An experimental ontology language formalized in Coq with many semantics
jinxinglim/coq-formalized-divide-and-conquer
This respository contains the formalization of different variations of divide-and-conquer algorithm design paradigm for lists. As a case study, we will see how these different variations lead to different sorting algorithms.
kaist-cp/view-hw
Mechanized Proof for Article: "Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8" (PLDI 2021)
rudynicolop/TAPL-Coq
Coq implementations of and proofs of properties of typed-languages in Benjamin Pierce's Types and Programming Languages
thery/sudoku
Sudoku in Coq