190 Open source projects that are alternatives of or similar to Formal Type Theory

Homotopy type theory

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

A selection of formal proofs in Coq.

Automation for de Bruijn syntax and substitution in Coq

Combinatorial species in HoTT

Total Parser Combinators in Coq

Verifying concurrent crash-safe systems

Certified Relational to Imperative

Bidirectional programming in Haskell with monadic profunctors

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

A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧

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

A framework for implementing and certifying impure computations in Coq

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

(WIP) Dependently-typed programming language with Agda style dependent pattern matching

Coq plugin for parametricity [[email protected]]

KCoFI Pudding: The formal proofs for the KCoFI system

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

Cosette is an automated SQL solver.

Implementation of sprintf for Coq

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

Formal Reasoning About Programs

A Hello World program in Coq.

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

Cryptographic Primitive Code Generation by Fiat

Formalisation of the linear lambda calculus in Coq

Porn browser formally-verified in Coq

Coq code accompanying several articles on semantics of functional programming languages

A compiler plug-in to control object lifetimes in Scala

An introductory tutorial for the Coq proof assistant.

A Certified Interpreter for ML with Structural Polymorphism

Formalization of C++ for verification purposes.

SoftwareFoundations(Ja)

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

The CompCert formally-verified C compiler

A Coq library for extensional finite sets and comprehension

Towards changing things and see if it proofs

Coq proofs of exercises in Pierce's book

Implementation of Nuprl's type theory in Coq

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

Normalization by evaluation for Martin-Löf Type Theory with dependent records

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

Programming language agnostic type construction language based on polynomials.

A framework for formally verifying distributed systems implementations in Coq

λΠ Programming Language Theory

Verified vector clocks, with Coq!

Experimental implementation of Cubical Type Theory

RISC-V Specification in Coq

This repo is the new home of Proof General

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

Mathematical Components

The Penn Locally Nameless Metatheory Library

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 ⭐️

A collection of papers on modules.

A Verified Compiler for Gallina, Written in Gallina

Collapsing Towers of Interpreters