Calculating correct compilers II: Return of the register machines

Bahr, Patrick; Hutton, Graham

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.

Citation

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

• 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
• DOI: https://doi.org/10.1017/s0956796820000209
• Keywords: Software
• Public URL: https://nottingham-repository.worktribe.com/output/4847230
• Publisher URL: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/calculating-correct-compilers-ii-return-of-the-register-machines/194A3C46A13A0BFDDE85976E96232AEC