An application of algebra to the semantics of programming languages

This dissertation investigates the use of the algebraic style of abstract data type specifications for the definition of programming language semantics. The choice of appropriate mathematical models for such presentations is an important aspect of this work largely because the semantics of programming languages will generally be defined in terms of domains that are more complex than those required for dealing with more elementary data types. The relationship between initial algebra semantics and the proposed style of specification is explored. From this foundation, the intuitive notion of the congruence of a pair of semantic definitions can be inspected and formalised against an algebraic background. Using the formal definition so developed and the simple but powerful notion of initiality, proofs of congruence are possible for semantics that are not amenable to the more traditional techniques of structural and fixed-point induction. Finally the problem of establishing the correctness of a compiler is investigated, reworking the traditional "commuting square" approach for the style of semantic presentation developed in this thesis rather than the usual initial algebra style. This allows a clearer focus on some of the shortcomings of the commuting square notion