Joint work with Robert J. Simmons.


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 logical correspondence mirrors the Reynolds functional correspondence, but we manipulate semantic specifications encoded in a logical framework instead of manipulating functional programs. Natural semantics and abstract machines are instances of substructural operational semantics. As a byproduct, using a substructural logical framework, we bring concurrent and stateful models into the domain of the logical correspondence.


Robert J. Simmons and Ian Zerny. A Logical Correspondence between Natural Semantics and Abstract Machines. Proceedings of the 2013 ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2013). ACM Press, 2013. To appear. [BIB].

Official website for PPDP’13.