Abstract In ‘Calculating Correct Compilers’ (Bahr & Hutton, 2015), 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.

@article{BahrH20,
  title = {Calculating correct compilers II: Return of the register machines},
  author = {PATRICK BAHR and GRAHAM HUTTON},
  journal = {Journal of Functional Programming},
  volume = {30},
  year = {2020},
  doi = {10.1017/s0956796820000209}
}