Girard (1998): Light Linear Logic (LLL)
What it does.
Girard introduces LLL, a subsystem of linear logic designed so that cut-elimination runs in polynomial time. The key move is to constrain duplication via boxes and a special “paragraph” modality (often written §\mathsf{§}§), which implements a stratification (depth discipline) over proofs. Promotion (the source of duplication) is permitted only in tightly controlled contexts, so the size and depth of proof nets cannot blow up during normalization. This yields an implicit characterization of PTIME via proofs-as-programs. ScienceDirect+1
Why it matters for SLLL.
LLL is the prototype for “light logics”: enforce structural restrictions (rather than explicit resource counters) to guarantee complexity bounds. Our SLLL uses a level modality ↑\uparrow↑ and uniform-level duplication to achieve the same goal with more explicit typing and agent-facing semantics.
Baillot & Mazza (2010): Linear Logic by Levels and Bounded Time Complexity
What it does.
This paper generalizes Girard’s depth-based stratification by assigning integer levels to proof-net edges. Levels induce a stratification stricter (or looser) than depth, recovering Girard’s systems when “level = depth,” but allowing more flexibility. They prove that with appropriate level constraints, cut-elimination stays within elementary time or PTIME, giving new characterizations of complexity classes. Notably, they show one can avoid paragraph boxes (or restrict them to atoms) while keeping the same complexity properties—useful for more efficient type assignment. arXivScienceDirectACM Digital Library+1
Why it matters for SLLL.
“Levels” are exactly the idea our ↑\uparrow↑-modality makes explicit at the type level. We adopt their insight that stratification can be decoupled from box depth, which makes typing and implementation cleaner for real agents (LLMs/GPUs).
Boudes, Mazza, Tortora de Falco (2015): An Abstract Approach to Stratification in Linear Logic
What it does.
This paper abstracts “stratification” into its own separate modality, defined by a general categorical construction that applies to any model of linear logic. They show that stratification need not be baked into the exponentials; however, when you connect it to exponentials, you recover the light-logic complexity bounds. They also give three reformulations of Baillot–Mazza’s “levels” (geometric, interactive, semantic), clarifying the landscape and unifying different presentations. arXivScienceDirectACM Digital LibraryDBLP
Why it matters for SLLL.
Exactly our philosophy: make stratification a first-class modality (our ↑\uparrow↑). Their categorical account justifies treating stratification independently and then coupling it to duplication to get provable PTIME bounds.
Murfet (2014/2017): Logic and Linear Algebra: an Introduction
What it does.
Murfet gives a friendly but deep tour of linear logic for algebraists, with concrete vector-space semantics of proofs as linear maps, emphasizing the cofree cocommutative coalgebra (Sweedler) for modeling the exponential !!!. It also connects to geometry of interaction intuitions. As a result, the semantics of promotion/duplication becomes linear-algebraic (coalgebraic) structure, which is great for building computable models and for seeing how resource sensitivity emerges algebraically. arXiv+1ResearchGate
Why it matters for SLLL.
A ready-made semantic playground for our system: the ↑\uparrow↑-modality and uniform-level !!
! can be interpreted over vector spaces/cofree coalgebras, helping to reason about soundness and potentially compile SLLL-typed agents to linear-algebraic runtimes (relevant for GPU/LLM backends).