• README ⤓ .txt 2026-07-17T121634.146 000000000000752
  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.
• Basic Logic ⤓ .md 2026-07-15T225637.000 000000000028144
  Sambin, Battilotti, and Faggian, "Basic logic: reflection, symmetry, visibility" (Journal of Symbolic Logic 65, 2000); roots in Sambin's formal topology and Battilotti's 1997 thesis. A sequent calculus B proposed as the base from which classical, intuitionistic, quantum, and non-modal linear logic are all obtained as extensions in a single framework, by adding structural rules while the operational rules stay fixed.
• Bounded Linear Logic ⤓ .md 2026-07-15T064403.000 000000000015360
  Girard, Scedrov, Scott (1992). Polynomial-time complexity via bounded exponentials. !ⁿA: at most n copies of A. Implicit computational complexity. Light and soft linear logic variants.
• Bunched Implications ⤓ .md 2026-07-15T055813.000 000000000022048
  O'Hearn and Pym introduced bunched implications (BI, 1999). Combines intuitionistic logic with linear/resource logic. Two conjunctions: additive (∧) and multiplicative (*). Foundation for separation logic. Substructural logic with resource sensitivity.
• Differential Linear Logic ⤓ .md 2026-07-17T120407.600 000000000000896
  Ehrhard and Regnier introduced differential linear logic (2003, 2006). Adds differentiation to linear logic. Derivative of proofs: ∂/∂x. Models smooth functions in denotational semantics. Foundation for differential λ-calculus and resource calculi.
• Geometry of Interaction ⤓ .md 2026-07-16T001736.000 000000000034408
  Jean-Yves Girard, "Geometry of interaction I: interpretation of System F" (1989), and the sequence through GoI V (1989–2011). Danos and Regnier's "Local and asynchronous beta-reduction" (1993, 1995) gave the path-algebra reading; Abramsky, Haghverdi, and Scott's "Geometry of interaction and linear combinatory algebras" (2002) gave the categorical axiomatization; Mackie's The Geometry of Interaction Machine (1995) built a compiler from it.
• Intuitionistic Dependence Logic ⤓ .md 2026-07-16T004347.000 000000000033240
  Samson Abramsky and Jouko Väänänen, "From IF to BI" (Synthese, 2009), which introduced the implication and named the connection it exposes; Fan Yang, "Expressing second-order sentences in intuitionistic dependence logic" (2010), proved the expressive power. The second of the two routes from dependence logic to full second-order logic, and the one nobody expected.
• Intuitionistic Linear Logic ⤓ .md 2026-07-16T004643.000 000000000035304
  Implicit in Girard (1987) as the intuitionistic fragment; Girard and Lafont, "Linear logic and lazy computation" (1987), gave the first term calculus; Benton, Bierman, de Paiva, and Hyland, "A term calculus for intuitionistic linear logic" (1993), gave the one that stuck, and Bierman's thesis (1993) the categorical semantics. Hyland and de Paiva's FILL (1993) is the full-intuitionistic variant.
• Light Linear Logic ⤓ .md 2026-07-15T061329.000 000000000019336
  Girard introduced Light Linear Logic (LLL, 1998). Captures polynomial time computation. Restricts linear logic's exponentials. Implicit computational complexity (ICC). Proofs normalize in polytime. Extends to Elementary Linear Logic (ELL) for elementary time.
• Linear Logic ⤓ .md 2026-07-15T071424.000 000000000018112
  Girard (1987). Resource-sensitive logic. Formulas as resources, used exactly once. Multiplicative/additive distinction. Foundation for concurrency, quantum, and programming language theory.
• Session Types ⤓ .md 2026-07-15T062133.000 000000000018304
  Honda introduced session types (1993). Types for communication protocols. Describe sequences of send/receive operations. Ensure protocol compliance at compile time. Corresponds to linear logic propositions.
• Soft Linear Logic ⤓ .md 2026-07-17T120407.600 000000000000832
  Lafont (2004). Polynomial time. Controlled contraction. Light logic variant. Foundation of implicit complexity.
• Subexponential Logic ⤓ .md 2026-07-15T071226.000 000000000015040
  Danos, Joinet, Schellinx (1993). Nigam and Miller (2009). Multiple exponential modalities. Fine-grained resource control. Foundation for logic programming semantics.
• Substructural Type Systems ⤓ .md 2026-07-15T074657.000 000000000014840
  Walker (2005), Turner. Linear types in practice. Affine, relevant, ordered restrictions. Resource management via types. Foundation for safe programming.
• CRITERIA ⤓ .txt 2026-07-17T120407.600 000000000000768
  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.