Dependent Types

Open-source projects categorized as Dependent Types | Edit details

Top 23 Dependent Type Open-Source Projects

  • 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.

    Project mention: Ask HN: What technology is “cutting edge” in 2022? | | 2022-01-23
  • FStar

    A Proof-oriented Programming Language

    Project mention: My favourite Pokémon is python | | 2022-01-09

    Consider that F* is a real language inspired by F#... could we create a C#-style language for program verification?

  • Scout APM

    Less time debugging, more time building. Scout APM allows you to find and fix performance issues with no hassle. Now with error monitoring and external services monitoring, Scout is a developer's best friend when it comes to application development.

  • Kind

    A modern proof language (by kind-lang)

    Project mention: Rust-like memory management with dependent types | | 2021-12-22
  • Agda

    Agda is a dependently typed programming language / interactive theorem prover.

    Project mention: Ask HN: What technology is “cutting edge” in 2022? | | 2022-01-23
  • Idris2

    A purely functional programming language with first class types

    Project mention: Idris 2: Quantitative Type Theory in Practice | | 2022-01-24

    I was a bit disappointed with linearity in QTT as I couldn't figured out how to create a safe API around a resizable array.

    The example given in the paper is a LinArray ( Unfortunately, as the community discovered, a user can "leak" a non-linear binding outside of the `newArray` constructor (which is what attempts to enforce linearity for all bindings). With multiple unrestricted handles, a user can accidentally double-free for instance. (

    The fundamental issue in this case is that linearity in QTT is a property of the parameter bindings and _not_ the type itself, meaning we can't easily express linearity as a _global_ property of the type.

    On the other hand, only affecting the parameter bindings makes it really easy to use runtime-erased/comptime stuff without reimplementing a bunch of common types as runtime- and comptime-only versions.

    ATS chooses the other path and makes linearity and runtime-erasure a part of the type (not without paying a hefty syntactic cost however).

  • juvix

    Juvix empowers developers to write code in a high-level, functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment and execution.

    Project mention: Missing line in a smart contract leads to $10M hack | | 2021-05-16

    I dont know how hard it would be to port it to other platforms. Different Virtual machine.

    Tezos uses a human readable stack based language as a low level represenation that is suited for formal proofs:

    If archetype depends on that then its going to be hard to port but i dont think it does.

    Another interesting project in development is which targets more backends beside michelson like llvm and wasm. Might run on eth2/Ewasm.

    There are also blockchain specific features like:

  • magmide

    A dependently-typed language intended to make provably correct code possible for working software engineers.

    Project mention: My Path to Magma | | 2021-12-04

    The Magma name requires disambiguation:

    His Magma programming language:

    > The goal of this project is to: create a programming language and surrounding education/tooling ecosystem capable of making formal verification and provably correct software mainstream and normal among working software engineers.

    Magma computer algebra system:

    > Magma is a computer algebra system designed to solve problems in algebra, number theory, geometry and combinatorics. It is named after the algebraic structure magma. It runs on Unix-like operating systems, as well as Windows.

  • SonarQube

    Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.

  • singletons

    Fake dependent types in Haskell using singletons

    Project mention: Hey Rustaceans! Got an easy question? Ask here (12/2021)! | | 2021-03-22

    In Haskell, you can do this with various trickery involving GADTs/constraints/singletons.

  • poprc

    A Compiler for the Popr Language

    Project mention: Programming languages without dynamic memory allocation? | | 2022-01-08

    Verilog, VHDL, and other hardware description languages, because you’re limited to the physically connected memory. Popr can be used as an HDL, so it also must work without dynamic allocation.

  • Coq-Equations

    A function definition package for Coq

    Project mention: Learn coq or agda before diving into idris2? | | 2021-05-02

    I'd say Agda is more similar to Idris than Coq. Coq has a different syntax and isn't as good for programming with dependent types as Agda and Idris (Agda and Idris both put a huge emphasis on dependent pattern matching, something that Coq only recently gained support for through the Equations package).

  • cubical

    Implementation of Univalence in Cubical Sets (by simhu)

  • ttlite

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

    Project mention: Seemingly Impossible Functional Programs | | 2021-10-28

    One of the authors of this work, who apparently now works on supercompilers at Meta, open sourced some nice tools for equivalence testing based on graph rewriting [1] and MLTT [2]. If you're interested in that kind of stuff I recommend checking out his work:



  • tensor-safe

    A Haskell framework to define valid deep learning models and export them to other frameworks like TensorFlow JS or Keras.

  • aya-dev

    ~ Who's generalizing definitional equalities?

    Project mention: Aya: a dependently-typed programming language | | 2021-08-15
  • hoq

    A language based on homotopy type theory with an interval

  • anders

    🧊 Anders: CCHM HTS

    Project mention: Anders CCHM/HTS Theorem Prover | | 2022-01-20
  • first-class-families

    First-class type families

  • cicada

    Cicada Language

    Project mention: Ask HN: What technology is “cutting edge” in 2022? | | 2022-01-23
  • awesome-rust-formalized-reasoning

    An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

    Project mention: Awesome-Rust-Formalized-Reasoning | | 2021-04-11
  • type-natural

    Type-level well-kinded natural numbers.

  • eliminators

    Dependently typed elimination functions using singletons

  • helf

    Haskell implementation of the Edinburgh Logical Framework

  • lens-typelevel

    Type-level lenses using singletons because why not

NOTE: The open source projects on this list are ordered by number of github stars. The number of mentions indicates repo mentiontions in the last 12 Months or since we started tracking (Dec 2020). The latest post mention was on 2022-01-24.

Dependent Types related posts


What are some of the best open-source Dependent Type projects? This list will help you:

Project Stars
1 coq 3,622
2 FStar 2,187
3 Kind 2,090
4 Agda 1,719
5 Idris2 1,536
6 juvix 279
7 magmide 257
8 singletons 253
9 poprc 183
10 Coq-Equations 168
11 cubical 134
12 ttlite 108
13 tensor-safe 96
14 aya-dev 81
15 hoq 78
16 anders 76
17 first-class-families 73
18 cicada 57
19 awesome-rust-formalized-reasoning 56
20 type-natural 32
21 eliminators 24
22 helf 22
23 lens-typelevel 15
Find remote jobs at our new job board There are 30 new remote jobs listed recently.
Are you hiring? Post a new remote job listing for free.
OPS - Build and Run Open Source Unikernels
Quickly and easily build and deploy open source unikernels in tens of seconds. Deploy in any language to any cloud.