1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19

\begin{gather*}
    \inferrule[Return]
      {Γ ⊢ t₁ : X₁ \quad ... \quad Γ ⊢ tₙ : Xₙ}
      {Γ \Vdash \mathsf{return}(t₁,...,tₙ) : X₁,...,Xₙ} \quad
     \inferrule[Variable]
      {\quad}
      {(xᵢ : Xᵢ) ∈ Γ ⊢ xᵢ : Xᵢ} \\
    \inferrule[Value Generator]
      {Γ ⊢ t₁ : X₁ \quad ... \quad Γ ⊢ tₙ : Xₙ}
      {Γ ⊢ f(t₁,...,tₙ) : Y} \\
    \inferrule[Pure Generator]
      {y₁ : Y₁, ..., yₘ : Yₘ, Γ \Vdash p : Z₁,...,Zₘ 
      \quad Γ ⊢ t₁ : X₁, ... , Γ ⊢ tₙ : Xₙ}
      {Γ \Vdash g(t₁, ..., tₙ) → y₁, ..., yₘ ⨾ p : Z₁, ...,Zₘ} \\
    \inferrule[Effectful Generator]
      {y₁ : Y₁, ..., yₘ : Yₘ, Γ \Vdash p : Z₁,...,Zₘ 
      \quad Γ ⊢ t₁ : X₁, …, Γ ⊢ tₙ : Xₙ}
      {Γ \Vdash h(t₁, ..., tₙ) ↝ y₁, ..., yₘ ⨾ p : Z₁, ..., Zₘ}
  \end{gather*}