[xmonad] StackSet patch
dons at galois.com
Mon May 4 12:29:18 EDT 2009
Let us know if you need any help.
> I found a really minor bug in the "new" function in StackSet.hs. I've
> attached a patch to fix it.
> More interesting, however, is how I found this. I've been transcribing
> XMonad's StackSets to the functional language/proof assistant Coq. I've
> set up a darcs repository with my work so far:
> darcs get www.cs.nott.ac.uk/~wss/repos/StackSet
> At the moment I have a fairly complete implementation of StackSets in
> Coq. I have to admit that I did cut a few corners here and there, but
> there's nothing that can't be fixed with a bit more work. From this Coq
> file, you can (in principle) extract Haskell code that is pretty close to
> the current StackSet.hs.
> I should emphasize that I haven't proven much about StackSets just yet.
> This only shows that the definitions in StackSet.hs can be made total
> (i.e. non-crashing and terminating) in a richer type theory. It should be
> fun to prove some QuickCheck properties in Coq – which is what I'd like
> to do next.
> xmonad mailing list
> xmonad at haskell.org
More information about the xmonad