  The first-order theory of MALL (multiplicative, additive linear logic) over
only equalities is an interesting but weak logic since it cannot capture
unbounded (infinite) behavior. Instead of accounting for unbounded behavior via
the addition of the exponentials (! and ?), we add least and greatest fixed
point operators. The resulting logic, which we call muMALL, satisfies two
fundamental proof theoretic properties: we establish weak normalization for it,
and we design a focused proof system that we prove complete. That second result
provides a strong normal form for cut-free proof structures that can be used,
for example, to help automate proof search. We show how these foundations can
be applied to intuitionistic logic.
