Actually, just spun around in circles from my semantics homework. The mission, should you choose to accept it, Take Lazy PCF, extend it w/ a mutable store, define an operation and denotation semantics. Now prove the two semantics coincide using logical r…
more »