@hackage linearscan1.0.0

The linearscan library is an implementation -- in Coq, extracted to Haskell -- of a register allocation algorithm developed by Christian Wimmer. It is described in detail in his Masters thesis, which can be found at http://www.christianwimmer.at/Publications/Wimmer04a/Wimmer04a.pdf. A Java implementation of this same algorithm, by that author, is used in Oracle's Graal project. It has also been implemented in C++ by Mozilla.

This version of the algorithm was written and verified in Coq, containing over 231 proved lemmas, at over 10K LOC. It was funded as a research project by BAE Systems (http://www.baesystems.com), to be used in an in-house compiler written in Haskell.

In order for the Coq code to be usable from Haskell, it is first extracted from Coq as a Haskell library, during which many of Coq's fundamental types are mapped directly onto counterparts in the Haskell Prelude.

This library's sole entry point is the function LinearScan.allocate, which takes a list of basic blocks, and a functional characterization of those blocks, and produces a new list, with register allocations applied to their component operations.