Linear logic

Summary

Linear logic, introduced by Jean-Yves Girard in 1987, is a logic in which hypotheses are resources that must be used exactly once. It drops the structural rules of weakening and contraction, and allows them back only for formulas marked with the exponentials $!$ and $?$. As a result, conjunction and disjunction split into multiplicative and additive versions. It has applications in proof theory, the semantics of programming languages and the theory of concurrency.