Abstract
Fifty years ago, John McCarthy and James Painter published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a register-based machine. In this article, we revisit this example in a modern context, and show how such a compiler can now be calculated directly from a specification of its correctness using simple equational reasoning techniques.
| Original language | English |
|---|---|
| Article number | 20 |
| Journal | Journal of Functional Programming |
| Volume | 27 |
| Number of pages | 11 |
| ISSN | 0956-7968 |
| DOIs | |
| Publication status | Published - 20 Sept 2017 |
Keywords
- program calculation
- verified compiler
- virtual machine
- Coq
- equational reasoning