Graded bases, Simply RaTT, and SLL2 signatures

The common parameter is one preordered semiring. Linear Base has linear functions and graded boxes; Graded Base has graded functions and a fully graded context. The direct translation preserves typing, one-step source reduction by target multisteps, and source equations. The reverse is a call-by-name CPS translation with the same type and operational claims but only the stated beta and modal beta–eta equations. Neither result states an inverse, completeness, normalization, or full abstraction.

The effect monoid and coeffect semiring are separate parameters, together with one of eight distributive-law formats and its matched-pair operations. The exact judgment has linear assumptions, discharged assumptions, $T_{e}A$, and $D_{r}A$. The source proves linear and coeffectful substitution; orienting the typed equations for the fragment without primitive operations preserves the complete judgment; and the categorical semantics validates the equational theory. No progress theorem or transfer to another effect system is claimed.

The exact imported package is source Progress Theorem 6.6, restricted Preservation Theorem 6.7, Borrow Safety Lemma 6.8 and Theorem 6.9, Uniqueness Corollary 6.10, and Equational Soundness Theorem 6.11. Preservation retains the non-function payload restriction and the scaled heap-compatibility context. Borrow safety retains the incoming permission-sum-one premise; Uniqueness additionally requires the source uniqueness type.

The signature includes Fitch contexts, stable types, guarded recursion, and the two-heap machine. The local derivations expose the source Fundamental Property 6.3, Productivity 3.1, and Causality 3.2. The space statement excludes old-heap retention by typed temporal machinery; it does not bound explicit stable accumulators. Jeffrey’s predecessor card is limited to the interval interpretation of LTL and its causal constrains type; it contributes no heap theorem. Switch, scan, and the Lustre-style $\mathsf{Flow}A=\mathsf{Str}(\mathsf{Maybe}A)$ are Simply RaTT library programs, not new primitive rules.

The separate ${\lambda }_{[\tau ]}$ signature uses value judgments $\mathrm{\Gamma }⊢V:X$, computation judgments $\mathrm{\Gamma }⊢M:X!\tau$, modalities $[\tau ]X$, and time markers $⟨\tau ⟩$. Its exact imported package is Progress 3.7, Preservation 3.10 with ${\tau }_S+\tau ={\tau }_{S^{\prime }}+{\tau }^{\prime }$, Equational Soundness 4.9, and Corollary 4.10. The Agda archive does not contain the proof of Theorem 4.9. A primitive clock-indexed ${\mathsf{Flow}}_{c}A$ rule and any theorem combining this state with Simply RaTT are explicitly conjectural.

Soft promotion and multiplexing replace ordinary exponential rules. External reduction strictly decreases $W_u(n)$, giving unique normal form in at most $W_u(n)$ steps. The polynomial corollary fixes the generic net and its degree. The representation theorem has conclusion ${\mathsf{S}}^{(\mathrm{deg}P+\mathrm{deg}Q+1)}⊢\mathsf{B}$, where the superscript counts antecedent copies rather than exponential layers. Neither theorem is an AARA cost judgment or a theorem about arbitrary semiring grades.