一句话：将直接从正确性规约计算编译器的方法从栈式目标机扩展到寄存器机。
本文延续 Bahr 与 Hutton（2015）的“计算正确编译器”工作。该工作提出直接从编译器正确性规约出发，通过初等推理技术计算编译器，并已覆盖多种语言特性及其组合；但其目标机主要是基于栈的机器，而真实编译器常面向基于寄存器的机器。本文说明如何将这一计算式方法自然地适配到寄存器机，从而为寄存器目标编译器的推导提供统一途径。摘要未报告具体案例细节或实验数据，主要贡献是方法论扩展。
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.