file.pdf (150.4 kB)

A Logical Correspondence between Natural Semantics and Abstract Machines

Download (150.4 kB)
journal contribution
posted on 01.01.1981 by Robert J. Simmons, Ian Zerny

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 substructurallogical framework, we bring concurrent and stateful models into the domain of the logical correspondence.

History

Publisher Statement

All Rights Reserved

Date

01/01/1981

Exports

Exports