Skip to content
<awesome-gh-repos>
vic

HigherOrderCO/Kind

A modern proof language
Source code at GitHub https://higherorderco.com
HigherOrderCO/Kind.json
{
  "createdAt": "2018-07-13T03:08:55Z",
  "defaultBranch": "master",
  "description": "A modern proof language",
  "fullName": "HigherOrderCO/Kind",
  "homepage": "https://higherorderco.com",
  "language": "Haskell",
  "name": "Kind",
  "pushedAt": "2025-01-22T16:54:12Z",
  "stargazersCount": 3709,
  "topics": [
    "dependent-types",
    "formality",
    "functional-programming",
    "lambda-calculus",
    "moonad",
    "proof-language",
    "proof-languages",
    "theorem-prover",
    "type-theory"
  ],
  "updatedAt": "2025-11-27T05:58:28Z",
  "url": "https://github.com/HigherOrderCO/Kind"
}

Kind

Section titled “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

Section titled “Usage”

  1. Clone and install this project

  2. Use the kind command to check/run terms

We will write a proper README later (: