[xmonad] xmonad in Coq

Wouter Swierstra wouter.swierstra at gmail.com
Fri Jan 13 10:14:36 CET 2012

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:


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,


More information about the xmonad mailing list