Bend 2: a fast language that blocks AI mistakes via proof. Install: curl -fsSL https://bend-lang.com/install.sh | sh
-
Updated
Sep 20, 2026 - TypeScript
#
dependent-types
Here are 341 public repositories matching this topic...
The Rocq Prover is an interactive theorem prover, or proof assistant. 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.
-
Updated
Sep 19, 2026 - OCaml
A modern proof language
dependent-types functional-programming lambda-calculus type-theory theorem-prover formality moonad proof-language proof-languages
-
Updated
Jan 22, 2025 - Haskell
A Proof-oriented Programming Language
programming-language dependent-types ocaml theorem-proving verification f-sharp proof-assistant smt c-language fstar interactive-theorem-proving program-proof dijkstra-monads
-
Updated
Sep 20, 2026 - F*
A purely functional programming language with first class types
-
Updated
Sep 18, 2026 - Idris
Agda is a dependently typed programming language / interactive theorem prover.
-
Updated
Sep 20, 2026 - Haskell
Lean Theorem Prover
-
Updated
Oct 14, 2023 - C++
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
dependent-types coq logic verification formal-methods type-safety formal-verification systems-programming
-
Updated
May 14, 2026 - Rocq Prover
A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧
programming-language rust typechecker dependent-types compiler type-theory systems-language type-system systems-programming bidirectional-typechecking dependent-record-types dependent-records
-
Updated
May 16, 2021 - Rust
A menagerie of cute implementations of modern typechecking algorithms
-
Updated
Sep 13, 2026 - Rust
Proof assistant based on the λΠ-calculus modulo rewriting
-
Updated
Sep 18, 2026 - OCaml
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
rust dependent-types logic theorem-proving formal-verification prover automated-theorem-provers reasoning theorem-prover constructive-mathematics proof-assistants
-
Updated
May 27, 2026
A fast functional language based on two level type theory
-
Updated
Jan 6, 2023 - Haskell
Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
-
Updated
Oct 23, 2023 - Agda
A Haskell library for typesafe music composition
haskell dependent-types midi music-composition haskell-library music-notation type-level-programming
-
Updated
Mar 3, 2019 - Haskell
A proof assistant and a dependently-typed language
-
Updated
Jun 8, 2026 - Java
A garden of small programming language implementations 🪴
dependent-types interpreter type-theory programming-languages compilers type-checking l-systems interpreters elaboration compilation typechecking normalization-by-evaluation type-systems language-garden
-
Updated
Sep 13, 2026 - OCaml
🚧 (Alpha stage software) A declarative data definition language for formally specifying binary data formats. 🚧
language programming-language rust parser dependent-types compiler binary-data dsl declarative data-description-language type-system statically-typed type-checker binary-format dependent-record-types
-
Updated
Sep 6, 2023 - Rust
A Compiler for the Popr Language
language dependent-types functional compiler concatenative verilog logic-programming non-deterministic partial-evaluators supercompiler linear-logic popr popr-compiler high-level-synthesis
-
Updated
Jan 7, 2021 - C
CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory
-
Updated
Aug 31, 2026 - OCaml
Add this topic to your repo
To associate your repository with the dependent-types topic, visit your repo's landing page and select "manage topics."