To reason about programs written in a language, one needs to define its formal semantics, derive a reasoning mechanism (e.g. a program logic), and maximize the proof automation. Unfortunately, a compiler may involve multiple languages and phases; it is tedious and error prone to do so for each language and each phase. We present an approach based on the use of higher order logic to ease this burden. All the Intermediate Representations (IRs) are special forms of the logic of a prover such that IR programs can be reasoned about directly in the logic. We use this technique to construct and validate an optimizing compiler. New techniques are used to compile-with-proof all the programs into the logic, e.g. a logic specification is derived automatically from the monad interpretation of a piece of assembly code. © 2011 Springer-Verlag.
CITATION STYLE
Li, G. (2011). Validated compilation through logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6664 LNCS, pp. 169–183). https://doi.org/10.1007/978-3-642-21437-0_15
Mendeley helps you to discover research relevant for your work.