Quantitative Separation Logic

Origin. Atkey introduced quantitative type theory (2018). Quantitative separation logic (QSL) by various authors. Tracks resource quantities, not just separation. Coefficients count resource usage. Foundation for linear/graded types.

Models. Counting resource usage. Separation logic: disjoint resources. Quantitative: how many times resources used. Coefficients from semiring: 0, 1, ω, etc. Graded modalities: !ᵣA means r copies of A.

Formalism.

Resource semiring: (R, 0, 1, +, ·) with:

0: no usage
1: exactly once
ω: unlimited
+: combined usage
·: sequential usage

Graded modality: !ᵣA: r-many A resources. !₀A: zero copies (erased at runtime). !₁A: exactly one copy (linear). !ωA: unlimited copies (intuitionistic).

Quantitative context: Γ = x₁ :ᵣ₁ A₁, ..., xₙ :ᵣₙ Aₙ Variables with usage annotations.

Typing rules: Variable: x :₁ A ⊢ x : A

Abstraction: Γ, x :ᵣ A ⊢ t : B ──────────────────── Γ ⊢ λx.t : !ᵣA → B

Application: Γ ⊢ f : !ᵣA → B Δ ⊢ a : A ────────────────────────────── Γ + r·Δ ⊢ f a : B

Heap with quantities: l ↦ᵣ v: location l holds v with r permissions. Fractional permissions: r = ½ for shared read.

Symbols.

Symbol	Unicode	Meaning
P^n	—	assertion with potential n
↦^n	—	points-to with potential
tick	—	consume one unit
*	—	separating conjunction

Metatheory. Type safety: well-typed programs don't misuse resources. Coefficients track usage precisely. Erasure: 0-quantified terms erased at runtime. Linear types as special case (R = {0,1,ω}). QTT: full dependent types.

Applies to. Resource-aware programming. Linear/affine types. Memory management. Rust ownership (informally). Certified resource bounds. Secure information flow.

Limitations. Annotation burden. Semiring choice matters. Tool support emerging. Inference challenging. More complex than simple separation. Interaction with effects.