Kernel Operational Semantics

The small-step operational semantics of Dart Kernel is given by an abstract machine in the style of the CEK machine. The machine is defined by a single step transition function where each step of the machine starts in a configuration and deterministically gives a next configuration. There are several different configurations defined below.

x ranges over variables, ρ ranges over environments, K ranges over expression continuations, E ranges over expressions, V ranges over values.

Environments are finite functions from variables to values. &rho[x → V] denotes the environment that maps x to V and y to ρ(y) for all y &neq; x.

An expression configuration indicates the evaluation of an expression with respect to an environment and an expression continuation.

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

An expression continuation configuration indicates application of an expression continuation to a value and an environment. The environment is threaded to the continuation because expressions can mutate the environment.

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