LINEAR LOGIC
Logics that drop both weakening and contraction, treating hypotheses as resources consumed exactly once, with the exponential modalities ! and ? reintroducing the discarded structural rules in a controlled way. Formulas are actions or resources rather than stable truths, and the multiplicative/additive distinction between connectives becomes primary.
Entries are organized from the core calculus outward. Linear logic proper anchors the subdivision, with its proof-net presentation. Resource-refined fragments (bounded, light, soft, subexponential linear logic) calibrate the exponentials for complexity control; differential linear logic adds a dual to promotion. Bunched implications combines a linear and an additive context. Session types appear as the resource discipline applied to communication.