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.

Abstract

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.

BibTeX.
Send e-mail to obtain a paper copy.