152 Open source projects that are alternatives of or similar to Peacoq

Combinatorial species in HoTT

Certified Relational to Imperative

Total Parser Combinators in Coq

Coq executable semantics and resource verifier

Formal Reasoning About Programs

A blog about Coq

Automation for de Bruijn syntax and substitution in Coq

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

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

Bidirectional programming in Haskell with monadic profunctors

Mathematical Components

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

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

A Verified Compiler for Gallina, Written in Gallina

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

A framework for implementing and certifying impure computations in Coq

The mathematical study of type theories, in univalent foundations

KCoFI Pudding: The formal proofs for the KCoFI system

Coq plugin for parametricity [[email protected]]

Cosette is an automated SQL solver.

Collapsing Towers of Interpreters

This repo is the new home of Proof General

Implementation of sprintf for Coq

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

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

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

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

Formalisation of the linear lambda calculus in Coq

The Penn Locally Nameless Metatheory Library

Coq code accompanying several articles on semantics of functional programming languages

Coq Support for Visual Studio Code

An introductory tutorial for the Coq proof assistant.

Porn browser formally-verified in Coq

Formalization of C++ for verification purposes.

SoftwareFoundations(Ja)

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

A Certified Interpreter for ML with Structural Polymorphism

A Coq library for extensional finite sets and comprehension

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

Coq proofs of exercises in Pierce's book

The CompCert formally-verified C compiler

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

RISC-V Specification in Coq

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

Implementation of Nuprl's type theory in Coq

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

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

Homotopy type theory

Cryptographic Primitive Code Generation by Fiat

A compiler plug-in to control object lifetimes in Scala

Verified vector clocks, with Coq!

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

Formal proof of the Four Color Theorem

Verifying concurrent crash-safe systems

A Hello World program in Coq.