Towards a framework for building formally verified supercompilers in Coq

Abstract

We present an on-going project for the development - in Coq - of a language-agnostic framework for building verified supercompilers. While existing supercompilers are not very big in size, they combine many different program transformations in intricate ways, so checking the correctness of their implementation presents challenges. We propose to define the main supercompilation algorithm in terms of abstract operations, which hide the details of the object language. The verification of the generic supercompiler relies then on properties of these operations, which are easier to establish in isolation, for each specific language. While we still need to try the approach on more supercompilers for specific languages, the framework in its current state appears a promising technique for simplifying the formal verification of supercompilers. © 2013 Springer-Verlag.