rzk
Proof assistant
An experimental proof assistant built on top of a type theory for synthetic ∞-categories.
An experimental proof assistant based on a type theory for synthetic ∞-categories.
205 stars
10 watching
10 forks
Language: Haskell
last commit: 14 days ago category-theoryhaskellhomotopy-type-theoryproof-assistant
Related projects:
| Repository | Description | Stars |
|---|---|---|
 andrew-johnson-4/lsts | A programming language and proof assistant built around type theory and lambda calculus. | 114 |
 liamoc/holbert | An interactive proof assistant designed to help with educational mathematics | 161 |
 amintimany/categories | An implementation of category theory in the Coq proof assistant. | 93 |
 the-little-prover/j-bob | A proof assistant with a formal system for verifying mathematical theorems and proofs | 420 |
 ecrancemerce/trakt | Automates goal preprocessing in proof automation tactics using a custom-built tool | 14 |
 jetbrains/arend | A theorem prover and a programming language based on Homotopy Type Theory | 694 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 0xzkml/zk-mnist | A demo project that integrates machine learning and zero-knowledge proof verification in a web application using TypeScript. | 119 |
 ditto/ditto | An experimentally designed dependently typed programming language with a focus on type checking and research | 173 |
 jwiegley/category-theory | An axiomatic formalization of category theory in Coq for personal study and practical work | 754 |
 chris-taylor/aima-haskell | An implementation of popular AI algorithms in the Haskell programming language | 331 |
 supranational/sppark | A high-performance library for accelerating zero-knowledge proof generation operations on GPUs | 185 |
 nalinbhardwaj/zordle | A web application built using Zero-Knowledge Proof technology to verify players' knowledge of word mappings without revealing the words themselves. | 215 |
 ekmett/hask | Category theory for Haskell with a strong lens-like flavor. | 161 |
 eashanhatti/konna | An experimental language exploring two-level type theory to achieve compile-time evaluation of dynamic features | 11 |