dedukti - Programming language

home edit

dedukti is a programming language created in 2009.

#873on PLDB

15Years Old

Download source code:

git clone https://github.com/Deducteam/Dedukti

Homepage · Source Code

Implementation of the λΠ-calculus modulo rewriting

Tags: programming language
dedukti is developed on GitHub and has 155 stars
Early development of dedukti happened in https://github.com/Deducteam
dedukti is written in OCaml, Bourne shell, Markdown, Make, Lisp, XML, YAML, Vim script, Python

Example 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).

Language features

Feature	Supported	Example	Token
MultiLine Comments	✓	(; A comment ;)	(; ;)
Comments	✓	(; This is a comment ;)
Semantic Indentation	X