Lambda Calculus with state:

where: new allocate a new memory location x and return pointer (initialize x to 0) !e deref a pointer e := e, which is assigning the pointee of the memory location at the first argument to the second argument new \begin{equation} \frac{l \not \in dom(S)}{E,S \vdash \text{new} \to l, S[l=0]} \end{equation} that is, we need to return to ourselves a new place in memory dereference \begin{equation} \frac{E, S_0 \vdash e \to l, S_1}{E, S_0 \vdash !e \to S_{1}(l), S_1} \end{equation} assignment \begin{equation} \frac{\begin{align} &E, S_0 \vdash e_1 \to I, S_1 \ &E, S_1 \vdash e_2 \to v, S_2 \end{align}}{ E, S_0 \vdash e_1 := e_2 \to v, S_2[I=v]} \end{equation} store a store is a mapping from memory locations to values—

where, 1 is stored at location l_{1}, and 42 is stored at location l_2 importantly! locations are first class—we can return pointers some observations the store is an extra argument in the environment the store is never copied: no evaluation step uses more than one store, and every store is modified at most once the state is unstructured; the whole store is passed to every step of the evaluation even if only a part is used semantics is very costly sequential order of evaluation must be defined (otherwise your state will be inconsistent) there are uncontrolled amount of aliasing of names unstructured states exposes too much since we only look up a few things at a time