152 Open source projects that are alternatives of or similar to Collapsing Towers

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

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.

Formalisation of the linear lambda calculus in Coq

Coq proofs of exercises in Pierce's book

IO for Gallina

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

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

The CompCert formally-verified C compiler

Convert Haskell source code to Coq source code

An introductory tutorial for the Coq proof assistant.

A Coq library for extensional finite sets and comprehension

Formal verification of OCaml programs

Verified vector clocks, with Coq!

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

A Certified Interpreter for ML with Structural Polymorphism

A framework for formally verifying distributed systems implementations in Coq

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

Cryptographic Primitive Code Generation by Fiat

The Penn Locally Nameless Metatheory Library

A Coq IDE build on top of Proof General's Coq mode

Coq code accompanying several articles on semantics of functional programming languages

Verified Software Toolchain

Implementation of Nuprl's type theory in Coq

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

Formalization of C++ for verification purposes.

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

Implementation of sprintf for Coq

Certified Relational to Imperative

A framework for implementing and certifying impure computations in Coq

KCoFI Pudding: The formal proofs for the KCoFI system

A Hello World program in Coq.

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

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

Cosette is an automated SQL solver.

Formal Reasoning About Programs

Total Parser Combinators in Coq

This repo is the new home of Proof General

Coq executable semantics and resource verifier

Mathematical Components

Verifying concurrent crash-safe systems

Tricks you wish the Coq manual told you

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

An introductory course to Homotopy Type Theory

Coq plugin for parametricity [[email protected]]

A gently curated list of companies using verification formal methods in industry

Combinatorial species in HoTT

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

A blog about Coq

Coq encoding of ZFC and formalization of the textbook Elements of Set Theory

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

A proof of Abel-Ruffini theorem.

Bidirectional programming in Haskell with monadic profunctors

Automation for de Bruijn syntax and substitution in Coq

A compiler plug-in to control object lifetimes in Scala

Porn browser formally-verified in Coq

Homotopy type theory

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