Need help with Kei?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

126 Stars 3 Forks GNU General Public License v3.0 71 Commits 1 Opened issues


A small and expressive dependently typed language

Services available


Need anything else?

Contributors list

# 480,290
67 commits
# 724,249
1 commit

Kei Language

Kei is a dependently typed language with a small and expressive core based on λΠ-calculus modulo rewriting.

The Core

The core of Key is based on a type theory called Lambda-Pi-Calculus Modulo Calculus. Despite the core being very experimental, Kei can prove some properties through an encoding of a typed rule.

Rules of static symbols are defined as in Dedukti, for example, a sized list vector can be defined like :

Rule Vector : (forall (x : nat) -> Type).
Rule Nil : (Vector Z).
Rule Cons : (forall (x : nat) (y : A) (H : (Vector x)) -> (Vector (S x))).

Rewriting Rules is expressed like :

tail = (\(forall (n' : nat) (vec : (Vector n')) -> Maybe) | x vec => [
  vec of Maybe
    |{x' y H}(Cons x' y H) => (Surely x' H)
    |{}Nil => Nothing

One of the most interesting properties of Kei is you can combine statics symbols with rewriting rules to create another logic system, like COC. In λΠ-calculus modulo the conversion of terms is available between β-reduction and Γ-Reduction, this means that a type can be changed through a type relation of a rewriting rule. Of course, if there is a well-typed substitution rule σ(x).


As an example let's define syntactical equality :

Rule type : Type.
Rule ≡ : (forall (n : type) (n' : type) -> Type).
Rule refl : (forall (n : type) -> (≡ n n)).

Extend the symbols with a static type with a scheme for proving : ``` Rule eq_rect : (forall (n : type) (n' : type) (x : (≡ n n')) (a : type) (f : (forall (a : type) (a' : type) -> Type)) (H : (f a n)) -> (f a n')).

fsym = ((forall (x : type) (y : type) -> Type) | x y => (≡ y x)). symmetry = ((forall (x : type) (y : type) (H' : (≡ x y)) -> (≡ y x)) | x y H' => (eqrect x y H' x f_sym (refl x))). ```

You could ask yourself if you need always specific a symbol scheme for proving. The idea is that you able to working with different approaches and logic system, however, the small core of Kei is expressive enough for represent trivial and more complex proofs like induction proofs with a few numbers of statics symbols and rewriting rules through of composition of rules.


You may need GHC and...

git clone
cd src
ghc --make Checker.hs -o Kei
*put in your enviroment* 
export PATH="$PATH:~/.../Kei Language/src"

Checking if everything is okay

Go to folder examples and runs in that folder :

Kei foo

If everything is okay you should see a message like this:

Bar : Just Foo.

The "Just" is just that Kei can infer the construction evaluated. So, when you check the terms Kei automatically eval the EVAL expression and return the value.


(Source : Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice)

What wasn't implemented

  • Totally Checker
  • Confluent Pattern Matching (avoid non Left-Linear Rules), this topic is a bit complicate Dedukti do a optimization of - patterns matching to solve this.
  • Impossible clause
  • Patterns matching clauses checking
  • Confluent Checker
  • A backend :)
  • Fast type checking


This work is very influenced by :
Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice (Ronan Saillard).
The λΠ-calculus Modulo as a Universal Proof Language (Mathieu Boespflug1, Quentin Carbonneaux2 and Olivier Hermant3).
Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory (Ali Assaf1, et al).

Besides the designer language like syntax was defined with the help of thoughts of Lucas and Davidson.

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.