TARGET LANGUAGE:

integers i
non-negative integers n
heap location names p
register names r  (includes esp)
stack variable names P
stack location variable names L

d = base | next(d)
l = L | base | next(l) | p
t = int | Nonsense | HeapPtr(t) | Single(l) | All[D](G,S)
S = l:Q
Q = P | Empty | t::S | Q /\ {l:t}
w = i | nonsense | p | d | w[l] | w[Q]
o = r | w | o[l] | o[Q]
ins = mov r,o
    | add r1,o
    | sub r1,o
    | load r,[r + i]
    | store [r + i],r
    | heapalloc r = <o>
    | jumpif0 r, o
    | (L,r) = unpack(o)
v = block | <w>
block = all[D](G,S) b
b = ins;b | jump o

D = {} | L,D | P,D
H = {...,p->t,...}
G = {...,r->t,...}

h = {...,p->v,...}
g = {...,r->w,...}
s = empty | w::s

The notation {...,X->Y,...} indicates a partial function from X to Y.

===============================================================================