Logical Specification of Operational Semantics

Abstract

Various logic-based frameworks have been proposed for
specifying the operational semantics of programming languages and
concurrent systems, including inference systems in the styles advocated by
Plotkin and by Kahn, Horn logic, equational specifications, reduction
systems for evaluation contexts, rewriting logic, and tile logic.
We consider the relationship between these frameworks, and assess their
respective merits and drawbacks - especially with regard to the modularity
of specifications, which is a crucial feature for scaling up to practical
applications. We also report on recent work towards the use of the Maude
system (which provides an efficient implementation of rewriting logic) as
a meta-tool for operational semantics.