We define general transformations on ASM specifications of programming
  language semantics. These transformations preserve
  the semantics of the programming language and can thus be used for
  the definition of correct compilations. Additionally, we define an
  extensible language AL for the specification of dynamic programming
  language semantics and describe how this allows reuse of verified
  transformations.  Together with a library of object-oriented
  verified implementations this leads to a framework for the
  construction of correct compilers based on the formal specification of
  source and intermediate language.