Calculating correct compilers II: Return of the register machines. (20th August 2020)

• Record Type: Journal Article
• Authors: BAHR, PATRICK; HUTTON, GRAHAM
• Is Part Of: Journal of functional programming. Volume 30(2020)
• Publication Date: 2020-08-20
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796820000209
• Languages: English
• ISSNs: 0956-7968

Abstract

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.