Top 218 Coq open source projects

Some unstructured notes concerning the Broad tutorial to take place in March 2020

Partial Commutative Monoids

This is a Coq formalization of Damas-Milner type system and its algorithm W.

Wnix /bin/cat wike (≡^-ω-^≡) - concatenate fi-fiwes awnd pwint own de standawd output

xmonad in Coq

Deprecated project!!! See Hermes-Lite2 at main web site

Repo for code from my NYC Haskell Users' Group talk on Oct. 24, 2014

A formally verified high-level synthesis tool based on CompCert and written in Coq.

No description, website, or topics provided.

LL(1) parser generator verified in Coq

A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.

A micro V language compiler

No description, website, or topics provided.

A formalization of finite, constructive log analysis using linear temporal logic

DMA source and sink blocks for Xilinx Zynq FPGAs

Problem Sets for MIT 6.822 Formal Reasoning About Programs, Spring 2021

A library of mechanised undecidability proofs in the Coq proof assistant.

Unicode tokeniser. Ucto tokenizes text files: it separates words from punctuation, and splits sentences. It offers several other basic preprocessing steps such as changing case that you can all use to make your text suited for further processing such as indexing, part-of-speech tagging, or machine translation. Ucto comes with tokenisation rules …

No description, website, or topics provided.

The reliable way to import and update a bazillion products.

Grappling technique map

Template project for program verification in Coq

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

Compilation and Verification of Data-Centric Languages

Intermediate Memory Model (IMM) and compilation correctness proofs for it

Tools and Examples for IcoBoard

TangNano-9K-example project

Adding extensions to DOT calculus

Where my everyday research happens

Fork of http://compcert.inria.fr/

A category theory library built on top of Homotopy Type Theory, by Jason Gross

A framework for extensible, reflective decision procedures.

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

Implementation for the book <Implementing functional languages: a tutorial>

Formalization of the polymorphic lambda calculus and its parametricity theorem

Writeup that goes along with this:

Formal verification of the Algorand consensus protocol

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

Coq library for tactics, basic definitions, sets, maps

SystemVerilog testbench for an Ethernet 10GE MAC core

No description, website, or topics provided.

XJTU-Tripler is based on HiPU100, an FPGA-friendly DNN accelerator, developed by CAG, Institute of AI & Robotics, XJTU.

a capability-based system

Lecture material for DeepSpec Summer School 2018

Foundational Cryptography Framework for machine-checked proofs of cryptography.

A Coq library for parametric coinduction

A Formal Library about Elliptic Curves for the Mathematical Components Library.

ITMO/CTD notes

No description, website, or topics provided.

Hardware of sampling model