QUESTION 5 Solution Hints ======================================================== There is no longer a division between the environment and the store. We have only a "State": State = Id -> Storable Storable = Int + Proc Proc = State -> State The key clauses: D : Declaration -> State -> State D[[ var I ]] = lam s. declare(I, s) // adds I to s, // initializes to {I: inInt(0)} C : Command -> State -> State C[[ I = E ]] = lam s. update(I, E[[ E ]]s, s) // any update goes C[[ call I ]] = lam s. case (find(I, e)) of inInt(n): error // must check that I names a Proc inProc(p): p(s) E : Expression -> State -> Storable E[[ N ]] = lam s. inInt( (int)N ) E[[ { B } ]] = inProc( B[[ B ]] ) // what seems to be missing here? B : Block -> State -> State B[[ D ; C ]] = lam s. SOMETHING LIKE THIS: let s' = mark s check( (lam s''. releaseTo(s', s'')), C[[ C ]](D[[ D ]]s') ) WHERE releaseTo "forgets", up to the mark s, all the local vars created by D and updated by C. The "function space", State = Id -> Storage, must be modelled with some form of namespace stack.