Skip to main content

Research Repository

Advanced Search

Calculating correct compilers II: Return of the register machines

Bahr, Patrick; Hutton, Graham


Patrick Bahr


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.


Bahr, P., & Hutton, G. (2020). Calculating correct compilers II: Return of the register machines. Journal of Functional Programming, 30,

Journal Article Type Article
Acceptance Date Jun 21, 2020
Online Publication Date Aug 20, 2020
Publication Date 2020
Deposit Date Aug 24, 2020
Publicly Available Date Feb 21, 2021
Journal Journal of Functional Programming
Print ISSN 0956-7968
Electronic ISSN 1469-7653
Publisher Cambridge University Press (CUP)
Peer Reviewed Peer Reviewed
Volume 30
Article Number e25
Keywords Software
Public URL
Publisher URL


You might also like

Downloadable Citations