The (Algebraic) Congruence of Two Programming Language Definitions

Clem Baker-Finch. In Science of Computer Programming, 4, 1990, pages 81-96.

Abstract

Since the beginning of the development of Scott-Strachey denotational semantics, one of the most useful formal results required by practitioners has been the congruence of dissimilar definitions of the semantics of some programming languages. While appropriate techniques are well-established, such proofs are undeniably difficult especially for the common case where one definition is operational and the other is denotational. In this paper we demonstrate an alternative proof technique that we believe is much simpler and more direct for cases involving an operational semantics. We proceed by reworking the example presented by Stoy in "The Congruence of Two Programming Language Definitions." Our approach is fundamentally algebraic and depends on a slightly different (we believe more appropriate) foundation of operational semantics.

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