176 Open source projects that are alternatives of or similar to imm

Coq formalizations of functional languages.

Proof of concept to generate safe and fast JavaScript

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

Formalisation of the linear lambda calculus in Coq

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

A framework for formally verifying distributed systems implementations in Coq

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Recipe for FPGA cooking

A minimalistic blockchain consensus implemented and verified in Coq

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

A library for formalizing Haskell types and functions in Coq

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

No description or website provided.

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT

Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]

A work-in-progress language and compiler for verified low-level programming

Statements of famous theorems proven in Coq [maintainer=@jmadiot]

Build trust into your image by creating a blockchain certificate for it

A library of abstract interfaces for mathematical structures in Coq [[email protected]]

Formalization of the basic actuarial mathematics using Coq

We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

formalization of the Dependent Object Types (DOT) calculus

Mostly Automated Synthesis of Correct-by-Construction Programs

Goose converts a small subset of Go to Coq

Import OCaml programs to Coq 🐓 🐫

Interactive Coq Proofs in Vim

Randomized Property-Based Testing Plugin for Coq

Stable sort algorithms and their stability proofs in Coq

🐣 A blog engine written and proven in Coq

Solutions for the book "Language Proof and Logic".

A function definition package for Coq

Reference sheet for the Coq language.

Archive for all Coq related OPAM packages organized in various repositories

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

The Vellvm (Verified LLVM) coq development.

Verified hash-based AMQ structures in Coq

A Visual Studio Code extension for Coq [[email protected],@fakusb]

Coq plugin embedding elpi

Advent of Code 2018, in Coq! (https://adventofcode.com/2018)

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

A selection of formal proofs in Coq.

A Library for Representing Recursive and Impure Programs in Coq

Formalization of the polymorphic lambda calculus and its parametricity theorem

A formalization of geometry in Coq based on Tarski's axiom system

A mechanisation of Wasm in Coq

Formalization of Typed Assembly Language (TAL) in Coq

A curated set of links to formal methods involving provable code.

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

The Language for Smart Legal Contracts

Hääl - Anonymous Electronic Voting System on Public Blockchains

Voevodsky's original development of the univalent foundations of mathematics in Coq

Mindless, verified (erasably) coding using dependent types

A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]

A core language for rule-based hardware design 🦑

FSCQ is a certified file system written and proven in Coq

PeaCoq is a pretty Coq, isn't it?

A SuperCompiler for Martin-Löf's Type Theory

A Learning Environment for Theorem Proving with the Coq proof assistant

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