Skip to main content

Research Repository

Advanced Search

Calculating correct compilers

Bahr, Patrick; Hutton, Graham

Authors

Patrick Bahr



Abstract

In this article we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high- level semantics by systematic calculation, with all details of the implementation of the compilers falling naturally out of the calculation process. Our approach is based upon the use of standard equational reasoning techniques, and has been applied to calculate compilers for a wide range of language features and their combination, including arithmetic expressions, exceptions, state, various forms of lambda calculi, bounded and unbounded loops, non-determinism, and interrupts. All the calculations in the article have been formalised using the Coq proof assistant, which serves as a convenient interactive tool for developing and verifying the calculations.

Journal Article Type Article
Publication Date Sep 15, 2015
Journal Journal of Functional Programming
Print ISSN 0956-7968
Electronic ISSN 1469-7653
Publisher Cambridge University Press (CUP)
Peer Reviewed Peer Reviewed
Volume 25
Issue e14
APA6 Citation Bahr, P., & Hutton, G. (2015). Calculating correct compilers. Journal of Functional Programming, 25(e14), doi:10.1017/S0956796815000180
DOI https://doi.org/10.1017/S0956796815000180
Publisher URL http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=9961488&fileId=S0956796815000180
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf

Files

ccc.pdf (264 Kb)
PDF

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





You might also like



Downloadable Citations

;