190 Open source projects that are alternatives of or similar to Hott

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

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

A selection of formal proofs in Coq.

Research on integrating datalog & lambda calculus via monotonicity types

Programming language agnostic type construction language based on polynomials.

Certified Relational to Imperative

Combinatorial species in HoTT

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

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

IO for Gallina

A proof of Abel-Ruffini theorem.

Cryptographic Primitive Code Generation by Fiat

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

KCoFI Pudding: The formal proofs for the KCoFI system

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

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

Cosette is an automated SQL solver.

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

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

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

Ltac2 tutorial

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

This repo is the new home of Proof General

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

Mathematical Components

Formalisation of the linear lambda calculus in Coq

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.

A Coq library for extensional finite sets and comprehension

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

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

Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)

Coq proofs of exercises in Pierce's book

Convert Haskell source code to Coq source code

Coq code accompanying several articles on semantics of functional programming languages

Verified Software Toolchain

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

Fine-grain implementations of common lambda calculi in Haskell, tested with QuickCheck

Verified vector clocks, with Coq!

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

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

Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!

An introductory tutorial for the Coq proof assistant.

Formal verification of OCaml programs

A framework for formally verifying distributed systems implementations in Coq

Finite sets, finite maps, multisets and generic sets

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

Mtac in Agda

λΠ Programming Language Theory

Formalization of C++ for verification purposes.

Lecture note on Lambda Calculus and Types for FLOLAC

Formal Reasoning About Programs

Multinomials for the Mathematical Components library.

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

Experimental implementation of Cubical Type Theory

Implementation of sprintf for Coq

A Hello World program in Coq.