Substructural Logic
A logic obtained by removing one or more of the structural rules of sequent calculus (weakening, contraction, exchange). Linear Logic removes weakening and contraction; affine logic keeps weakening; relevant logic keeps contraction; ordered logics also remove exchange. Substructural systems make hypotheses behave like resources, the type-theoretic foundation of ownership types (Rust, Pony’s reference capabilities), region-based memory management, and capability-typed languages.