Bounded Linear Logic

Bounded linear logic (BLL) is a substructural logic that extends affine logic with explicit resource bounds. While affine logic tracks whether a resource can be duplicated at all, BLL tracks how many times — introducing a system of polynomial bounds on the use of hypotheses. This yields a type system in which memory allocation, iteration depth, and data structure size are statically controlled by the logical structure of proofs.

Developed by Martin Hofmann and others, bounded linear logic has been applied to certified compilation and to the verification of resource usage in embedded and real-time systems. The type system of BLL can be seen as a logical refinement of type theories that track usage through effect systems or ownership types.

Bounded linear logic demonstrates that resource limits need not be enforced by runtime monitors or garbage collectors. They can be enforced by the logical structure of the program itself. This is not an optimization technique. It is a change in what a type system is for: from guaranteeing correctness to guaranteeing capacity.