A Logical Correspondence between Natural Semantics and Abstract Machines

<p>We present a logical correspondence between natural semantics and abstract machines. This correspondence enables the mechanical and fully-correct construction of an abstract machine from a natural semantics. Our <em>logical correspondence</em> mirrors the Reynolds <em>functional correspondence</em>, but we manipulate semantic specifications encoded in a logical framework instead of manipulating functional programs. Natural semantics and abstract machines are instances of <em>substructural operational semantics</em>. As a byproduct, using a <em>substructural</em>logical framework, we bring concurrent and stateful models into the domain of the logical correspondence.</p>