coq-formalization

Verified hash-based AMQ structures in Coq

A formalization of category theory in the Coq proof assistant.

LVC verified compiler

A Lustre compiler in Coq

Formalization of C++ for verification purposes.

Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization

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.

Formalization of temporal logic in Coq

Formalising Turing Machines In Coq (bachelor's thesis)

Verimag Polyhedra Library

Paper: Formalizing line editors in Coq

les problèmes proposés par le journal Le Monde en Coq

A foundational framework for modular cryptographic proofs in Coq

A Coq formalisation of the R programming language

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.

Computing Pi decimal using Plouffe Formula in Coq

Formalization of Category Theory in Coq.

A fornalisation of Grobner basis in ssreflect

A proof of Fermat's theorem on sum of two squares with mathcom using gaussian integers.

Certified LambdaJS semantics and interpreter.

Fortune's algorithm described in coq

Uniform Interpolation for some Substructural Logics (work in progress)

Coq formalization of the Habanero programming model.

Work based on http://www-sop.inria.fr/marelle/GeometricAlgebra/

An experimental ontology language formalized in Coq with many semantics

Coq implementations of and proofs of properties of typed-languages in Benjamin Pierce's Types and Programming Languages