From f60b209eae598160f6cf160415e08ae72658cd32 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Wed, 13 Nov 2024 16:18:01 +0100
Subject: Initial structure

---
 readme.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 readme.md

(limited to 'readme.md')

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.
-- 
cgit v1.2.3