Kei – A small and expressive dependent language

Also a mumbo dumbo here, but I might be able to say something helpful. This is a bit of long post as I am trying to provide some context.

A useful way to think of logic and type systems is simply as rewrite rules on arbitrary strings. In logic we call these strings "theorems" and in type theory we call them "types".

In particular, say we have the logical theorem "a /\ (a -> b)". In classical (propositional) logic this corresponds to "a implies b, and a is true", so we make the (obvious) deduction that "b" is true. In other words, we rewrite "a /\ (a -> b)" with the string "b".

Intuitively, we want to say the above rewrite means the same thing as "(a /\ (a -> b)) -> b". However, the former is a rewrite while the later is just a static string. Thus we are forced to distinguish between the formal "->" character and the rewrite process, despite these naively/intuitively both meaning inference.

A bit of terminology. Classically, we call strings "theorems" and when we rewrite one string for another, we call that a "deduction". So say we have a string "S" and rewrite it as "T", a common way of notating such a deduction is "S => T". Furthermore, the whole system of deductions is what we call our "metalogic" while the collection of theorems produced is our "formal logic".

Anyway, so we have to distinguish between "->" and "=>", which seems a bit unfortunate. There is this standard tool in classical logic called the Deduction Theorem which adds a rule that given "S => T" we can deduce "S -> T". However, the justification for this uses somewhat sophisticated math and, by necessity, it's an argument in some (meta)metalogic. There are other ways of handling this and metalogics that don't have the Deduction Theorem at all. I have even read that Quantum Logic doesn't have such a rule and that adding it in turns the whole system into classical logic!

Now, to finally get to the point, Kei looks like it uses a metalogic it's calling "λ-Calculus Modulo Theory" which ports the Deduction Theorem to type theory, or in particular, the dependently typed λ-calculus. They seem to be calling these new rules Γ-reduction. In other words, it attempts to make general rewrite rules, like β-reduction, first-class citizens by adding types that correspond to said rules.

If I'm understanding correctly, one attractive feature of this is that it "closes the loop," per se, allowing one to encode their λ-Calculus Modulo Theory within itself, which by extension, let's us encode any other λ-calculus as well. Ostensibly, this should allow for maximally compact and expressive types, since you don't have to hack simple metalogical concepts into a less powerful type system.

I only skimmed their paper, but in general one could use their system to model some badly-behaved (i.e. non-confluent) type theories; however, they seem to have a (meta)theorems showing that certain uses of the Γ-reduction give you well-behaved ones.