Intuitionistic Linear Logic (ILL)

Origin. 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.

Models. Linear logic with one conclusion. Girard's LL is classical — involutive negation, ⅋, ?, and a two-sided duality — and it is beautiful and has no term calculus, because a proof with many conclusions is not a program. ILL drops ⅋, ⊥, and ?, makes ⊸ primitive rather than defined, and gets Curry–Howard back. Everything that uses linear logic in computing uses ILL.

Formalism.

Connectives: ⊗ tensor, ⊸ linear implication (primitive), & with, ⊕ plus, ! of course, 1, ⊤, 0. Absent: ⅋, ⊥, ?, and the involutive (−)⊥. Linear negation is not primitive: ¬A is A ⊸ 0, and it is not involutive.

Sequents: Γ ⊢ A — one conclusion, as in LJ. Γ is a multiset: exchange yes, weakening and contraction no.

Key rules: Γ ⊢ A Δ, A ⊢ B ───────────────── cut Γ, Δ ⊢ B

Γ, A ⊢ B ──────────── ⊸R Γ ⊢ A ⊸ B

!Γ ⊢ A ──────── !R (promotion: the context must be entirely !'d) !Γ ⊢ !A

The exponential's three rules: dereliction !A ⊢ A weakening Γ ⊢ B ⟹ Γ, !A ⊢ B contraction Γ, !A, !A ⊢ B ⟹ Γ, !A ⊢ B ! is exactly the modality that restores the structural rules, for the formulas that carry it.

Term calculus (Benton–Bierman–de Paiva–Hyland): Types are formulas; terms are proofs. ⊗ gives pairs that must both be consumed; & gives pairs of which one is chosen. ! gives promotion/dereliction as a comonadic pair. Subject reduction and strong normalization hold; cut elimination is β-reduction.

Categorical semantics: A symmetric monoidal closed category with finite products and a monoidal comonad for !. The linear–non-linear adjunction (Benton 1995): a monoidal adjunction between a cartesian category and a linear one, whose comonad is !. This is the model that stuck.

ILL vs FILL: FILL (Hyland–de Paiva) keeps ⅋, ⊥, ? and multiple conclusions while staying intuitionistic — all connectives independent, as in IPC. Harder, and less used.

Symbols.

Metatheory. The reason ILL and not LL is Curry–Howard: a single-conclusion sequent is a term with a type, and a multiple-conclusion one is not — which is why Girard's classical system, for all its symmetry, needed proof nets and the geometry of interaction before it had a computational reading, and ILL had one immediately. Benton's linear–non-linear adjunction is the semantics that survived: ! is not a primitive modality to be axiomatized but the comonad of a monoidal adjunction, which explains why its three rules come as a package. Every linear type system, every session-type discipline, and separation logic's resource reading descend from ILL rather than from LL.

Applies to. Linear and affine type systems. Session types. Quantum programming languages, where no-cloning is the absence of contraction. Bunched implications and separation logic. Any resource discipline with a term calculus — which is all of them.

Limitations. Dropping ⅋ and the involutive negation loses linear logic's duality, which was the point of Girard's system: ILL is what you get by giving up the symmetry to get the terms. It is not the intuitionistic fragment of LL in the naive sense — the translation is subtle, and FILL exists because getting a genuinely intuitionistic multiple-conclusion system is harder than restricting to one. And ! is decidedly not a comonad in the naive sense either: getting the coherence right took a decade and several wrong term calculi.

© 2026 Lingenic LLC