Initial structure

1 files changed, 12 insertions, 0 deletions

diff --git a/readme.md b/readme.md
new file mode 100644
index 0000000..2ab9678
--- /dev/null
+++ b/readme.md
@@ -0,0 +1,12 @@
+# mili
+
+> Linear lambda calculus with linear types, de Bruijn levels and
+> unbounded minimization
+
+Linear lambda calculus is a restricted version of the lambda calculus in
+which every variable occurs exactly once. This typically implies linear
+normalization and therefore Turing incompleteness.
+
+We extend the linear lambda calculus with bounded iteration and
+unbounded minimization such that it barely becomes Turing complete,
+while still benefitting from the advantages of syntactic linearity.