Top 23 Dependent Type Open-Source Projects

• coq

  87 4,616 10.0 OCaml

  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

  4 3,456 4.8 Rust

  A next-gen functional language (by HigherOrderCO)

  

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

• InfluxDB

  www.influxdata.com featured

  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.

  

• FStar

  42 2,570 9.9 F*

  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

  39 2,401 9.5 Idris

  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

  27 2,378 9.8 Haskell

  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

  22 804 6.6 Coq

  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

  2 282 5.6 Haskell

  Fake dependent types in Haskell using singletons

• SaaSHub

  www.saashub.com featured

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

  

• awesome-rust-formalized-reasoning

  3 265 7.6

  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

  1 257 0.0 Rust

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

  

• aya-dev

  1 241 9.2 Java

  ~ Youkai (∞, 1)-Mountain

  

• poprc

  4 233 3.2 C

  A Compiler for the Popr Language

• Coq-Equations

  1 211 6.8 Coq

  A function definition package for Coq

• cubical

  0 142 0.0 Haskell

  Implementation of Univalence in Cubical Sets (by simhu)

• ttlite

  1 121 0.0 Scala

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

• tensor-safe

  0 101 0.0 Haskell

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

• first-class-families

  1 85 6.2 Haskell

  First-class type families

• hoq

  0 82 0.0 Haskell

  A language based on homotopy type theory with an interval

• nominal

  3 66 4.0 TypeScript

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

  

• spidr

  4 62 5.9 Idris

  Accelerated machine learning with dependent types

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

• meta-cedille

  1 55 7.5 Agda

  Minimalistic dependent type theory with syntactic metaprogramming

• thorin2

  2 44 9.7 C++

  The Higher ORder INtermediate representation - next gen

  

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

• type-natural

  0 33 6.2 Haskell

  Type-level well-kinded natural numbers.

• eliminators

  0 27 4.5 Haskell

  Dependently typed elimination functions using singletons

• SaaSHub

  www.saashub.com featured

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

  

Dependent Types related posts

• Change of Name: Coq –> The Rocq Prover

  3 projects | news.ycombinator.com | 26 Dec 2023

• Idris2: A purely functional programming language with first class types

  1 project | news.ycombinator.com | 6 Nov 2023

• Accelerated machine learning with dependent types

  1 project | news.ycombinator.com | 30 Oct 2023

• Lean4 helped Terence Tao discover a small bug in his recent paper

  10 projects | news.ycombinator.com | 27 Oct 2023

• Types versus sets (and what about categories?)

  1 project | news.ycombinator.com | 31 Aug 2023

• Why Mathematical Proof Is a Social Compact

  1 project | news.ycombinator.com | 31 Aug 2023

• If given a list of properties/definitions and relationship between them, could a machine come up with (mostly senseless, but) true implications?

  5 projects | /r/math | 11 Jul 2023
• A note from our sponsor - SaaSHub
  www.saashub.com | 7 May 2024

  SaaSHub helps you find the best software and product alternatives Learn more →

Index

Sponsored

SaaSHub - Software Alternatives and Reviews

SaaSHub helps you find the best software and product alternatives

www.saashub.com