A linear first-order functional intermediate language for verified compilers

DOI10.1007/978-3-319-22102-1_23zbMATH Open1465.68042arXiv1503.08665OpenAlexW2208324330MaRDI QIDQ2945646FDOQ2945646

Authors: Sigurd Schneider, Gert Smolka, Sebastian Hack 

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1503.08665

Recommendations

• A verified compiler for an impure functional language
• Formal verification of coalescing graph-coloring register allocation
• A formally verified compiler back-end
• Pilsner: a compositionally verified compiler for a higher-order imperative language
• The verified CakeML compiler backend

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Cites Work

• Formalizing the LLVM intermediate representation for verified program transformations
• Grail: a functional form for imperative mobile code
• Concrete semantics. With Isabelle/HOL
• Correspondence between ALGOL 60 and Church's Lambda-notation
• A verified compiler for an impure functional language
• Optimal register allocation for SSA-form programs in polynomial time
• A linear first-order functional intermediate language for verified compilers
• Formal verification of coalescing graph-coloring register allocation

Cited In (5)

• Pilsner: a compositionally verified compiler for a higher-order imperative language
• A verified compiler for an impure functional language
• Verified spilling and translation validation with repair
• Formal verification of coalescing graph-coloring register allocation
• A linear first-order functional intermediate language for verified compilers

Uses Software

• Coq
• Vellvm

This page was built for publication: A linear first-order functional intermediate language for verified compilers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945646)