Dependent Types

Open-source projects categorized as Dependent Types
Edit details
Language: + Haskell + Rust + Idris + Coq + TypeScript + OCaml + F* + Java + C + Scala + Agda + C++
Topics: programming-language Haskell Data structures type-theory proof-assistant
The modern identity platform for B2B SaaS
The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
workos.com
Sponsored

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: Change of Name: Coq –> The Rocq Prover | news.ycombinator.com | 2023-12-26

    The page summarizing the considered new names and their pros/cons is interesting: https://github.com/coq/coq/wiki/Alternative-names

    Naming is hard...

  • Kind

    A next-gen functional language (by HigherOrderCO)

    • Project mention: Kind: A lambda-calculus based pure programming language | news.ycombinator.com | 2023-11-27

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo

  • FStar

    A Proof-oriented Programming Language

    • Project mention: Lean4 helped Terence Tao discover a small bug in his recent paper | news.ycombinator.com | 2023-10-27

  • Idris2

    A purely functional programming language with first class types

    • Project mention: Idris2: A purely functional programming language with first class types | news.ycombinator.com | 2023-11-06

  • Agda

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

    • Project mention: Types versus sets (and what about categories?) | news.ycombinator.com | 2023-08-31

    This was recently deemed inappropriate:

    "Bye bye Set"

    "Set and Prop are removed as keywords"

    https://github.com/agda/agda/pull/4629

  • magmide

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

    • Project mention: Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think? | /r/rust | 2023-07-04

    https://github.com/magmide/magmide when

  • singletons

    Fake dependent types in Haskell using singletons

  • WorkOS

    The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

    WorkOS logo

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

  • fathom

    🚧 (Alpha stage software) A declarative data definition language for formally specifying binary data formats. 🚧 (by yeslogic)

  • aya-dev

    ~ Youkai (∞, 1)-Mountain

  • poprc

    A Compiler for the Popr Language

  • Coq-Equations

    A function definition package for Coq

  • cubical

    Implementation of Univalence in Cubical Sets (by simhu)

  • ttlite

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

  • tensor-safe

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

  • cicada

    Cicada Language (by cicada-lang)

    • Project mention: Cicada – A FOSS, Cross-Platform Version of GitHub Actions and Gitlab CI | news.ycombinator.com | 2023-11-06

    There is a collision in names:

    Cicada, this CI tool, uses a DSL (domain specific language) to write configuration, and this DSL is referred to as "Cicada language", and blasted in marketing copy as a "real programming language" on https://cicada.sh/

    However, this is a completely different language from Cicada language, a programming language and theorem prover hosted at https://cicada-lang.org/ and https://github.com/cicada-lang/cicada

    This name collision is very confusing, and I wonder why Cicada the CI tool didn't just stick to python, since it is also a "real programming language"

  • first-class-families

    First-class type families

  • hoq

    A language based on homotopy type theory with an interval

  • nominal

    Powerful nominal types for your Typescript project (by Coder-Spirit)

  • spidr

    Accelerated machine learning with dependent types

    • Project mention: Accelerated machine learning with dependent types | news.ycombinator.com | 2023-10-30

  • meta-cedille

    Minimalistic dependent type theory with syntactic metaprogramming

  • thorin2

    The Higher ORder INtermediate representation - next gen

    • Project mention: Can one use lambda calculus as an IR? | /r/Compilers | 2023-06-06

  • type-natural

    Type-level well-kinded natural numbers.

  • SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
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).

Dependent Types related posts

Index

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

Project Stars
1 coq 4,602
2 Kind 3,438
3 FStar 2,562
4 Idris2 2,395
5 Agda 2,371
6 magmide 804
7 singletons 282
8 awesome-rust-formalized-reasoning 263
9 fathom 256
10 aya-dev 239
11 poprc 233
12 Coq-Equations 208
13 cubical 142
14 ttlite 118
15 tensor-safe 101
16 cicada 92
17 first-class-families 84
18 hoq 82
19 nominal 66
20 spidr 60
21 meta-cedille 54
22 thorin2 43
23 type-natural 33

Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com