Abstract

We present the first-order intermediate language IL for verified compilers. IL is a functional language with calls to a nondeterministic environment. We give IL terms a second, imperative semantic interpretation and obtain a register transfer language. For the imperative interpretation we establish a notion of live variables. Based on live variables, we formulate a decidable property called coherence ensuring that the functional and the imperative interpretation of a term coincide. We formulate a register assignment algorithm for IL and prove its correctness. The algorithm translates a functional IL program into an equivalent imperative IL program. Correctness follows from the fact that the algorithm reaches a coherent program after consistently renaming local variables. We prove that the maximal number of live variables in the initial program bounds the number of different variables in the final coherent program. The entire development is formalized in Coq.

Paper

ITP 2015 Paper at the PS Chair.

The paper has been accepted to ITP 2015 and will be available at the publisher's website shortly.

An extended version is available at arxiv.org.

ITP Presentation Slides

Slides

Coq Development

The Coq development is available on github: https://github.com/sigurdschneider/lvc
See README.md at Github for required Coq version and dependencies.

Coqdoc

Browse the development online:

Coqdoc (updated 2015-06-03)

Coqdoc (proofs suppressed, updated 2015-06-03)

Running an example

General build instruction can be found in README.md which is included in the repository. After building, the examples can be run from the command line. The Fibonacci-inspired example can be run with

./lvcc.native -3 true examples/fib.il

The option -3 true enables the translation from IL to IL/I (including parameter elimination).