A Constructive Approach to Compiler Correctness

  • Peter D. Mosses


It is suggested that denotational semantic definitions of programming languages should be based on a small number of abstract data types, each embodying a fundamental concept of computation. Once these fundamental abstract data types have been implemented in a particular target language (e.g. stack-machine code), it is a simple matter to construct a correct compiler for any source language from its denotational semantic definition. The approach is illustrated by constructing a compiler similar to the one which was proved correct by Thatcher, Wagner Et Wright ( 1979). Some familiarity with many-sorted algebras is presumed.
How to Cite
Mosses, P. (1980). A Constructive Approach to Compiler Correctness. DAIMI Report Series, 9(118). https://doi.org/10.7146/dpb.v9i118.6536