HigherOrderCO/Kind

A modern proof language

3,764

stars

279

commits

Haskell

primary language

Jan 22, 2025

updated

higherorderco.com

dependent-types

formality

functional-programming

lambda-calculus

moonad

proof-language

proof-languages

theorem-prover

type-theory

README

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 kind command to check/run terms

We will write a proper README later (:

Contributors

191 commits

41 commits

41 commits

4 commits

Similar repos

HigherOrderCO/KindBook

shared contributors

leanprover/lean

Lean Theorem Prover

2,153

shared topics

VictorTaelin/Interaction-Calculus

A programming language and model of computation that matches the optimal λ-calculus reduction…

948

shared contributors

cedille/cedille

Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda…

393

shared topics

VictorTaelin/AI-scripts

Some handy AI scripts

696

shared contributors

agda/agda

Agda is a dependently typed programming language / interactive theorem prover.

2,930

shared topics

sdiehl/write-you-a-haskell

Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)

3,484

shared topics

VictorTaelin/Formality

Languages

Haskell

100.0%

README

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 kind command to check/run terms

We will write a proper README later (: