linearscan: Linear scan register allocator, formally verified in Coq

[ bsd3, development, library ] [ Propose Tags ]

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 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 (, 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.




Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


  • No Candidates
Versions [RSS],,,,,,,,, 0.7.0, 0.8.0, 0.9.0, 0.10.0, 0.10.1, 0.10.2, 0.11, 0.11.1, 1.0.0
Dependencies base (>=4.7 && <5.0), containers, ghc-prim, mtl, transformers [details]
License BSD-3-Clause
Author John Wiegley
Revised Revision 1 made by JohnWiegley at 2022-06-24T20:47:23Z
Category Development
Home page
Source repo head: git clone
Uploaded by JohnWiegley at 2015-11-20T17:35:06Z
Distributions NixOS:1.0.0
Reverse Dependencies 2 direct, 0 indirect [details]
Downloads 10464 total (41 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2016-11-29 [all 3 reports]