In this paper we present a hierarchy of verified generic theories for 
compiling standard imperative language constructs using the specification and
verification system PVS. The hierarchy consists of specifications for
compiling assignments, control structures, and procedures into 
linearized assembly code.

The specifications are generic in the sense that they abstract from concrete
source and target languages; they specify an abstract compilation pattern
which can be instantiated.

Since each of these patterns can be formalized and verified separately,
the verification task is broken into small manageable steps.
A further modularization and reduction of complexity is achieved by splitting
the compilation of control structures into three steps: control structures are
first translated into a structure of blocks, then the 
blocks are linearized by introducing jump instructions, and finally, the
procedures are linearized.

Applicability of the generic theories to specific compilation processes is
demonstrated by means of two simple examples.