[xmonad] xmonad in Coq

[Wouter Swierstra]

Hi guys,

For a while I've been looking into formalizing parts of xmonad in the
Coq proof assistant. After a bit of work, I've written a Coq module
that, when you extract Haskell code from it, produces a drop-in
replacement for xmonad's StackSet module. The generated Haskell code
is clearly not hand-written and triggers plenty of ghc warnings, but
passes the QuickCheck testsuite. I've put everything online here:

  https://bitbucket.org/wouterswierstra/xmonad

It require one or two very modest patches to xmonad to build, but
nothing controversial. See the readme for more technical details.

I've managed to prove a handful of QuickCheck properties in Coq, but I
just don't have the time to see this project through. If anyone is
interested in contributing, I'd be very happy to advise them on how to
proceed. I think it would make quite a nice exercise for anyone
interested in learning more about formal verification using Coq -- but
it's certainly not for the faint hearted!

All the best,

  Wouter