Compiler generation from denotational semantics

Abstract

A methodology is described for generating provably correct compilers from denotational definitions of programming languages. An application is given to produce compilers into STM code (an STM or state transition machine is a flow-chart-like program, low-level enough to be translated into efficient code on conventional computers). First, a compiler ϕ: LAMC → STM from a lambda calculus dialect is defined. Any denotational definition Δ of language L defines a map (Formula presented.): L → LAMC, so (Formula presented.) compiles L into STM code. Correctness follows from the correctness of ϕ. The algebraic framework of Morris, ADJ, etc. is used. The set of STMs is given an algebraic structure so any (Formula presented.) may be specified by giving a derived operator on STM for each syntax rule of L. This approach yields quite redundant object programs, so the paper ends by describing two flow analytic optimization methods. The first analyzes an already-produced STM to obtain information about its runtime behaviour which is used to optimize the STM. The second analyzes the generated compiling scheme to determine runtime properties of object programs in general which a compiler can use to produce less redundant STMs.