@article{calccomp2,
  Title = {Calculating Correct Compilers II: Return of the Register Machines},
  Author = {Patrick Bahr and Graham Hutton},
  Year = {2020},
  Month = aug,
  Date = {2020-08-20},
  volume = {30},
  doi = {10.1017/S0956796820000209},
  journal = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  number = {e25},
  Abstract = {In 'Calculating Correct Compilers' we developed a new approach to
calculating compilers directly from specifications of their correctness.  Our
approach only required elementary reasoning techniques, and has been used to
calculate compilers for a wide range of language features and their
combination.  However, the methodology was focused on stack-based target
machines, whereas real compilers often target register-based machines.
In this article, we show how our approach can naturally be
adapted to calculate compilers for register machines.},
  Keywords = {program calculation, verified compiler, virtual machine, Rocq, preorder,register machines}
}