Bend 2: a fast language that blocks AI mistakes via proof. Install: curl -fsSL https://bend-lang.com/install.sh | sh
-
Updated
Nov 12, 2026 - TypeScript
GeezerVisonThe World Wide Web, restored to 800 pixels of glory. |
| Home|About|Gaming cabinet|Archives|How it works|Starter sites |
GeezerVison is showing github.com â Build software better, together
#
dependent-typesHere are 391 public repositories matching this topic...Language: All
Filter by language
Sort: Most stars
Sort options
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.
A modern proof language
dependent-types functional-programming lambda-calculus type-theory theorem-prover formality moonad proof-language proof-languages
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
A purely functional programming language with first class types
Agda is a dependently typed programming language / interactive theorem prover.
Lean Theorem Prover
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
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
A menagerie of cute implementations of modern typechecking algorithms
Proof assistant based on the ÎŧÎ -calculus modulo rewriting
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
Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
A fast functional language based on two level type theory
A Haskell library for typesafe music composition
haskell dependent-types midi music-composition haskell-library music-notation type-level-programming
A proof assistant and a dependently-typed language
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
ð§ (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
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
CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory
Add this topic to your repoTo associate your repository with the dependent-types topic, visit your repo's landing page and select "manage topics." |
| You are visitor 01402503 â GeezerVison does not store the pages you look up. Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800Ã600. No cookies required. |