Calculating Correct Compilers II: Return of the Register Machines

Patrick Bahr, Graham Hutton

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review


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.
Original languageEnglish
Article numbere25
JournalJournal of Functional Programming
Publication statusPublished - 20 Aug 2020


  • program calculation
  • verified compiler
  • register machines
  • preorder
  • Coq


Dive into the research topics of 'Calculating Correct Compilers II: Return of the Register Machines'. Together they form a unique fingerprint.

Cite this