# 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.