A Linear First-Order Functional Intermediate Language for Verified Compilers

TL;DR

This paper introduces a linear first-order intermediate language for verified compilers, providing a formal framework with semantic interpretations, a register assignment algorithm, and proofs of correctness, all formalized in Coq.

Contribution

It presents a novel linear first-order intermediate language with a formal semantics, a coherence property, and a verified register allocation algorithm, all formalized in Coq.

Findings

The register assignment algorithm is correct and produces coherent programs.

The number of live variables bounds the number of variables in the final program.

The entire development is formalized in Coq, ensuring rigorous correctness proofs.

Abstract

We present the linear 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.