Kernel Operational Semantics

Expression configuration	Next configuration
<x, ρ, K>expr	<K, ρ(x), ρ>cont
<x = e, ρ, K>expr	<e, ρ, VarSet(x, K)>expr

Expression continuation configuration	Next configuration
<VarSet(x, K), V, ρ>cont	<K, ρ[x → V]>cont