Open AccessA Constructive Approach to Compiler Correctness
Author(s) -
Peter D. Mosses
Publication year - 1980
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v9i118.6536
Subject(s) - compiler , programming language , computer science , correctness , construct (python library) , constructive , denotational semantics , compiler correctness , compiler construction , language construct , semantics (computer science) , theoretical computer science , operational semantics , process (computing)
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.