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.
Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, Ppdp '13, 2013, p. 109-119
Main Research Area:
Symposium on Principles and Practice of Declarative ProgrammingPrinciples and Practice of Declarative Programming, 2013