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 phi: LAMC -> STM from a lambda calculus dialect is defined. Any denotational definition DD of language L defines a map DD': L -> LAMC, so DD'_circle phi compiles L into STM code. Correctness follows from the correctness of phi.

The algebraic framework of Morris, ADJ, etc. is used. The set of STMs is given an algebraic structure so any DD'_circ phi 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.