Function-only evaluation-strategy translations

The $\mathsf{name}$ and $\mathsf{val}$ calculi share simply typed variables, abstraction, and application. Their reductions are compatible closures and differ only in the value premise on beta. The $\mathsf{let}$ calculus adds one explicit binding and four administrative rules; $\mathsf{need}$ adds garbage collection.

The $\mathsf{lin}$ calculus has base types, exponential types, linear functions, promotion, exponential elimination, and structural rules only for exponential assumptions. The $\mathsf{aff}$ target admits weakening for every assumption but still restricts contraction to exponential assumptions.

Name substitution and typing are lemma 37.5; linear and affine target subject reduction are theorem 37.4, corollary 37.11. The name, value, and need translations preserve and reflect reflexive-transitive reduction in theorem 37.6, theorem 37.9, theorem 37.12. Call-by-let conservativity is lemma 37.8.

The exact published theorem owner is [MOTW99], Propositions 2.1–6.7. The value reflection proof uses the source’s call-by-let reachable-image argument and its Proposition 5.4. The constants-and-primitives observational equivalence is not promoted to equality of reductions.

The signature contains no products, sums, recursion, effects, polymorphism, dependent types, deterministic evaluation contexts, heaps, or cost labels. No theorem establishes full abstraction, a one-update sharing cost, or correctness of an arbitrary lazy implementation.

The pinned Kappa companion translates finite syntax and classifies five principal examples. Its appendix E entry is implementation evidence, not mechanized metatheory.