diff options
Diffstat (limited to 'readme.md')
| -rw-r--r-- | readme.md | 12 |
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. |