Berger and Tratt [1]} gave program logic for
\(\text{Mini-ML}^\square _e\)  [2]}, which would
allow fine-grained reasoning about the behavior of code generators.
However, it cannot manipulate open code which ours can deal with.
