dedukti is an actively used programming language created in 2009.

11Years Old 132Users ?Jobs

Example code from the web:

Nat: Type.
zero: Nat.
succ: Nat -> Nat.
def plus: Nat -> Nat -> Nat.
[ n ] plus zero n --> n
[ n ] plus n zero --> n
[ n, m ] plus (succ n) m --> succ (plus n m)
[ n, m ] plus n (succ m) --> succ (plus n m).

Last updated August 9th, 2020

Edit dedukti on GitHub