Tue Jul 21 12:42:23 CEST 2009

growing higher level semantics

The overall problem is that it is quite straightforward to go from
high -> low by mapping a high level construct in a low level one, and
proving this map preserves the algebraic/logic structure.  Going the
other way is not possible in general because a lot of constructs will
lie outside of the range of the mapping.  (I.e. the lower-level
semantics does not have a structure to hold on to..)

So, in general, how do you build higher level semantics given an
operational one?