INCLUSION CRITERIA
An entry belongs in this subdivision if and only if its consequence relation omits both weakening and contraction, so that each hypothesis is used exactly once, typically with exponential modalities (!, ?) to recover the missing rules locally.
Required: At least one of the following:
- A sequent calculus or proof-net system lacking weakening and contraction
- Exponential modalities that mark reusable resources
- A resource-sensitive semantics (coherence spaces, phase semantics, game semantics) for such a calculus
Not sufficient: Dropping only contraction (Affine). Dropping only exchange (Ordered). Dropping weakening for a relevance criterion (Relevant).
Boundary: Bunched implications is cross-listed with Applications/Verification (separation logic). Session types are cross-listed with Type/Effects. Linear type systems that enforce single use through typing belong in Type; the pure proof theory and its semantics belong here.