Kind
A modern proof language
This repository is a full rewrite of Kind from the old JS implementation to Haskell. It is being actively developed. See examples on [KindBook](https://github.com/HigherOrderCO/KindBook). The project is written primarily in Haskell, distributed under the MIT License license, first published in 2018. It has gained significant community traction with 3,753 stars and 150 forks on GitHub. Key topics include: dependent-types, formality, functional-programming, lambda-calculus, moonad.
Kind
Kind is a minimal Proof Checker.
This repository is a full rewrite of Kind from the old JS implementation to
Haskell. It is being actively developed. See examples on
KindBook.
Usage
-
Clone and install this project
-
Use the
kindcommand to check/run terms
We will write a proper README later (:
Contributors
Showing top 6 contributors by commit count.
Related Repositories
rocq-prover/rocq
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.
FStarLang/FStar
A Proof-oriented Programming Language
idris-lang/Idris2
A purely functional programming language with first class types
agda/agda
Agda is a dependently typed programming language / interactive theorem prover.
leanprover/lean3
Lean Theorem Prover
magmide/magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.