152 Open source projects that are alternatives of or similar to Mindless Coding

Formalisation of the linear lambda calculus in Coq

Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors

Porn browser formally-verified in Coq

sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility

《软件基础》中译版 Software Foundations Chinese Translation

An introductory tutorial for the Coq proof assistant.

Formalising Type Theory in a modular way for translations between type theories

Coq proofs of exercises in Pierce's book

The CompCert formally-verified C compiler

Verified vector clocks, with Coq!

A port of Coq to Javascript -- Run Coq in your Browser

A compiler plug-in to control object lifetimes in Scala

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

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

Coq code accompanying several articles on semantics of functional programming languages

The Penn Locally Nameless Metatheory Library

Formalization of C++ for verification purposes.

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

A Coq library for extensional finite sets and comprehension

A Certified Interpreter for ML with Structural Polymorphism

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

SoftwareFoundations(Ja)

A framework for formally verifying distributed systems implementations in Coq

Implementation of Nuprl's type theory in Coq

Implementation of sprintf for Coq

This repo is the new home of Proof General

Collapsing Towers of Interpreters

A Hello World program in Coq.

The mathematical study of type theories, in univalent foundations

Verifying concurrent crash-safe systems

Coq executable semantics and resource verifier

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

Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.

Formal specification and verification of hardware, especially for security and privacy.

Combinatorial species in HoTT

CoqPIE (an IDE for the Coq theorem prover + PEDANTIC)

A blog about Coq

Automation for de Bruijn syntax and substitution in Coq

A framework for implementing and certifying impure computations in Coq

Certified Relational to Imperative

A Verified Compiler for Gallina, Written in Gallina

KCoFI Pudding: The formal proofs for the KCoFI system

Total Parser Combinators in Coq

An axiom-free formalization of category theory in Coq for personal study and practical work

Formal proof of the Four Color Theorem

Cosette is an automated SQL solver.

Coq plugin for parametricity [[email protected]]

Formal Reasoning About Programs

A Coq-based synthesis of Scala programs which are correct-by-construction

Bidirectional programming in Haskell with monadic profunctors

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

PeaCoq is a pretty Coq, isn't it?

Coq Support for Visual Studio Code

RISC-V Specification in Coq

Homotopy type theory