Patrick Bahr
Calculating correct compilers
Bahr, Patrick; Hutton, Graham
Abstract
© 2016 Cambridge University Press. 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.
Citation
Bahr, P., & Hutton, G. (2015). Calculating correct compilers. Journal of Functional Programming, 25, https://doi.org/10.1017/S0956796815000180
Journal Article Type | Article |
---|---|
Acceptance Date | Jul 17, 2015 |
Online Publication Date | Sep 16, 2015 |
Publication Date | 2015 |
Deposit Date | Apr 8, 2016 |
Publicly Available Date | Apr 8, 2016 |
Journal | Journal of Functional Programming |
Print ISSN | 0956-7968 |
Electronic ISSN | 1469-7653 |
Publisher | Cambridge University Press (CUP) |
Peer Reviewed | Peer Reviewed |
Volume | 25 |
Article Number | e14 |
DOI | https://doi.org/10.1017/S0956796815000180 |
Public URL | http://eprints.nottingham.ac.uk/id/eprint/32702 |
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
Calculating correct compilers II: Return of the register machines
(2020)
Journal Article
Liquidate your assets: reasoning about resource usage in liquid Haskell
(2019)
Journal Article
Call-by-need is clairvoyant call-by-value
(2019)
Journal Article
AutoBench: comparing the time performance of Haskell programs
(2018)
Conference Proceeding
Theorem proving for all: equational reasoning in Liquid Haskell (Functional Pearl)
(2018)
Conference Proceeding