Calculating Correct Compilers II: Return of the Register Machines

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.

Categories: Compilers, Formal Verification

Tags: Program Calculation, Verified Compiler, Virtual Machine, Coq, Preorder, Register Machines