Light Linear Logic

Light linear logic (LLL) is a refinement of linear logic introduced by Jean-Yves Girard to control the computational complexity of proof normalization. In LLL, the exponential modalities — which in full linear logic permit unbounded duplication and discarding — are restricted so that every typable term normalizes in polynomial time. This makes LLL not merely a logic but a programming language in which well-typed programs are guaranteed to run efficiently.

The central insight of LLL is that complexity bounds can be enforced by structural proof constraints rather than by explicit resource counters. This connects light linear logic to the broader program of implicit computational complexity, which seeks to characterize complexity classes through type discipline and logical structure rather than through machine models.

The significance of light linear logic is not that it produces efficient programs. It is that it reveals efficiency to be a structural property of proofs, not an extrinsic measurement. The programmer who writes in LLL is not merely coding; she is proving that her algorithm is efficient by the form of her reasoning.