  A desired but challenging property of compiler verification is
compositionality in the sense that the compilation correctness of a program can
be deduced from that of its substructures ranging from statements, functions,
and modules incrementally. Previously proposed approaches have devoted
extensive effort to module-level compositionality based on small-step semantics
and simulation theories. This paper proposes a novel compiler verification
framework based on denotational semantics for better compositionality.
Specifically, our denotational semantics is defined by semantic functions that
map a syntactic component to a semantic domain composed of multiple behavioral
\emph{sets}, and compiler correctness is defined by the behavioral refinement
between semantic domains of the source and the target programs. Therefore, when
proving compiler correctness, we can extensively leverage the algebraic
properties of sets. Another important contribution is that our formalization of
denotational semantics captures the full meaning of a program and bridges the
gap between those based on conventional powerdomains and what realistic
compiler verification actually needs. We demonstrate our denotation-based
framework viable and practical by applying it to the verification of the
front-end of CompCert and showing that the compositionality from the
compilation correctness of sub-statements to statements, from functions to
modules, and from modules to the whole program (i.e., module-level
compositionality) can be achieved similarly.
