In programming language theory, a closure is an unevaluated term Γ , A ⊢ e : B proves Γ 𝐴 𝑒 : 𝐵 \Gamma,A\vdash e:B along with a captured Environment ρ : 𝖤𝗇𝗏 Γ : 𝜌 𝖤𝗇𝗏 Γ \rho:\mathsf{Env}\;\Gamma .