The Coq mailing list

[Beta Ziliani <bziliani AT famaf.unc.edu.ar>]

Hi John,

I'd be interested to know what was the outcome of the project from the point of view of BEA Systems. Is there any report about it?

Many thanks,
Beta

Written from mobile. Excuse my limited communication.

On Nov 20, 2015 2:44 PM, "John Wiegley" <johnw AT newartisans.com> wrote:

linearscan[1] is a linear scan register allocator[2], written in Coq[3], and
extracted to Haskell, as a library for Haskell programs that need to allocate
registers. It may also be used directly from Coq.

This project is the result of a year-long effort, funded by BAE Systems[4], to
explore the application of dependent-types and mathematical verification to a
typical engineering task. During the course of construction, several hundred
theorems about the code were proven -- although exhaustive coverage was not,
in the end, achievable given our time constraints. To remedy this, and as a
test of the extraction to Haskell, an optional runtime verifier was built to
certify the resulting allocations.

Coq 8.5b2[5] was used, as well as the ssreflect[6] library created for that
version[7]. linearscan further relies on another library, coq-haskell[8], that
I created to facilitate inter-operation between Haskell and Coq.

For those using Hoopl[9] to represent program graphs, incorporating linearscan
is quite easy: provide an instance of NodeAlloc using the linearscan-hoopl[10]
library. Examples of doing so are provided in the test suite for that library.

The allocation algorithm implemented by this library was first written in Java
by Hanspeter Mössenböck and Michael Pfeiffer[11], and later improved upon by
Christian Wimmer[12], whose master's thesis provided the specification for our
implementation.

John Wiegley
BAE Systems

Footnotes:
[1]  http://hackage.haskell.org/package/linearscan

[2]  http://www.cs.ucla.edu/~palsberg/course/cs132/linearscan.pdf

[3]  https://coq.inria.fr/

[4]  http://www.baesystems.com/en-us/our-company/inc-businesses/electronic-systems/research-advanced-development/about-r-and-ad

[5]  https://coq.inria.fr/news/125.html

[6]  http://ssr.msr-inria.inria.fr/

[7]  http://ssr.msr-inria.inria.fr/FTP/

[8]  https://github.com/jwiegley/coq-haskell

[9]  https://hackage.haskell.org/package/hoopl

[10]  http://hackage.haskell.org/package/linearscan-hoopl

[11]  http://dl.acm.org/citation.cfm?id=647478.727924

[12]  http://www.christianwimmer.at/Publications/Wimmer04a/