In recent years, formal verification of computer systems of
increasing size has become practical.  Researchers have been able
to verify complex artifacts at a variety of abstraction levels
spanning from CPU designs to network protocols.

These achievements remain discrete efforts, but there has been
increasing interest in rendering them interoperable, as
exemplified by the DeepSpec project.  The ability to connect
correctness proofs of components verified at various levels of
abstraction would enable the construction of extremely reliable
heterogenous systems through end-to-end verification.

In this talk, we propose that a successful synthesis of existing
research on game semantics, refinement-based methods, abstraction
layers and logical relations has the potential to serve as a
common theory of certified components.  We apply this methodology
to define a compositional semantics for the verified compiler
CompCert, and demonstrate that the compiler's correctness proof
can be extended to this compositional setting much more easily
than using previous approaches.