An Algebraic Model for Operational Semantics and Proofs of Congruence
Clem Baker-Finch. In 14th Australian Computer Science Conference, Australian Computer Science Communications, 1991, pages 40.1-40.10.
It is generally accepted that the operational semantics of a
programming language is an abstract interpreter, so operational
definitions are considered to be specifications of a rule for
evaluating programs. However when considering their relation with a
denotational semantics of the same language, a little more precision
is required and the model of the operational semantics (the
mathematical object that `is' the abstract interpreter) must be
identified. Usually domain theory is invoked but it is argued in this
paper that a construction similar to that used in the initial algebra
approach to abstract data types is more appropriate. Moreover, such a
construction allows clarification of the notion of semantic
congruence and greatly simplifies the proofs of such relations.
to obtain a paper copy.