eval

Con entorno

ev '(MN) ρ = ↑^fun(ev 'M ρ) (ev 'N ρ)
ev '(λx.M) ρ = ↓_val(λε.ev 'M ρ['x → ε])
ev 'x ρ = ρ 'x

Con entorno y continuación

ev '(MN) ρ κ = ev 'M ρ (λε₁. ev 'N ρ (λε₂. ↑^fun(ε₁)ε₂κ))
ev '(λx.M) ρ κ = κ(↓_val(λε κ₁.ev 'M ρ['x → ε] κ₁))
ev 'x ρ κ = κ (ρ 'x)