The source formulas and terms of chapter 37 are 𝐴,𝐵::=𝑍∣𝐴→𝐵,𝑀,𝑁::=𝑥∣𝜆𝑥.𝑀∣𝑀𝑁. Contexts are finite maps with exchange. Besides the ordinary variable, abstraction, and application rules, their structural rules are Γ⊢𝑀:𝐵Γ,𝑥:𝐴⊢𝑀:𝐵S−WeakΓ,𝑥:𝐴,𝑦:𝐴⊢𝑀:𝐵Γ,𝑧:𝐴⊢𝑀[𝑥:=𝑧,𝑦:=𝑧]:𝐵S−Contr. The beta rule is unrestricted in 𝗇𝖺𝗆𝖾 and has a value premise 𝑉 ::=𝑥 ∣𝜆𝑥.𝑀 in 𝗏𝖺𝗅.
The 𝗅𝗂𝗇 target formulas and terms are 𝐴,𝐵::=𝑍∣!𝐴∣𝐴⊸𝐵,𝐿,𝑀,𝑁::=𝑥∣!𝑀∣𝜆𝑥.𝑀∣𝑀𝑁::=∣𝗅𝖾𝗍 !𝑥=𝑀 𝗂𝗇 𝑁. An assumption 𝑥 :𝐴 is linear and !𝑥 :!𝐴 is exponential. Context juxtaposition below requires disjoint variable domains. 𝑋𝑥:𝐴⊢𝑥:𝐴L−IdΓ,𝑥:𝐴⊢𝑀:𝐵Γ,!𝑥:!𝐴⊢𝑀:𝐵L−Der Γ⊢𝑀:𝐵Γ,!𝑥:!𝐴⊢𝑀:𝐵L−WeakΓ,!𝑥:!𝐴,!𝑦:!𝐴⊢𝑀:𝐵Γ,!𝑧:!𝐴⊢𝑀[𝑥:=𝑧,𝑦:=𝑧]:𝐵L−Contr !Γ⊢𝑀:𝐴!Γ⊢!𝑀:!𝐴L−Bang−IΓ⊢𝑀:!𝐴Δ,!𝑥:!𝐴⊢𝑁:𝐵Γ,Δ⊢𝗅𝖾𝗍 !𝑥=𝑀 𝗂𝗇 𝑁:𝐵L−Bang−E Γ,𝑥:𝐴⊢𝑀:𝐵Γ⊢𝜆𝑥.𝑀:𝐴⊸𝐵L−LamΓ⊢𝑀:𝐴⊸𝐵Δ⊢𝑁:𝐴Γ,Δ⊢𝑀𝑁:𝐵L−App. Here !Γ changes every 𝑥 :𝐴 in Γ to !𝑥 :!𝐴. Reduction is the compatible closure of (𝜆𝑥.𝑀)𝑁⟼𝗅𝗂𝗇𝑀[𝑥:=𝑁],𝗅𝖾𝗍 !𝑥=!𝑀 𝗂𝗇 𝑁⟼𝗅𝗂𝗇𝑁[𝑥:=𝑀],(𝗅𝖾𝗍 !𝑥=𝐿 𝗂𝗇 𝑀)𝑁⟼𝗅𝗂𝗇𝗅𝖾𝗍 !𝑥=𝐿 𝗂𝗇 (𝑀𝑁),𝗅𝖾𝗍 !𝑦=(𝗅𝖾𝗍 !𝑥=𝐿 𝗂𝗇 𝑀) 𝗂𝗇 𝑁⟼𝗅𝗂𝗇𝗅𝖾𝗍 !𝑥=𝐿 𝗂𝗇 (𝗅𝖾𝗍 !𝑦=𝑀 𝗂𝗇 𝑁).
The call-by-let source adds 𝗅𝖾𝗍 𝑥 =𝑀 𝗂𝗇 𝑁, its ordinary typing rule, and Let-I, Let-V, Let-C, and Let-A from definition 37.7. The call-by-need source adds Need-G. The affine target replaces L-Weak by Γ⊢𝑀:𝐵Γ,𝑥:𝐴⊢𝑀:𝐵A−Weak for arbitrary 𝐴, retains exponential-only contraction, and adds Aff-Weak. No source or target in this sheet contains products, sums, recursion, effects, or a deterministic evaluation-context rule.