Calculating correct compilers

Patrick Bahr, Graham Hutton

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

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.
Original languageEnglish
JournalJournal of Functional Programming
Volume25
ISSN1469-7653
DOIs
Publication statusPublished - 1 Sept 2015
Externally publishedYes

Keywords

  • program calculation, verified compiler, virtual machine, Coq, equational reasoning

Fingerprint

Dive into the research topics of 'Calculating correct compilers'. Together they form a unique fingerprint.

Cite this