xmonad in Coq
Coq Haskell
Pull request Compare This branch is 1 commit ahead, 4 commits behind wouter-swierstra:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
scripts
src
.gitignore
LICENSE
Makefile
README

README


This repository contains an implementation of xmonad's StackSet module
in Coq. Extracting Haskell from this Coq file produces a drop-in
replacement module for the original Haskell module (once it has been
massaged a bit by a few innocuous shell scripts).

The Makefile has mostly been generated by coq_makefile. It contains
several build targets:

  - make patched_xmonad -- downloads xmonad and applies several
  reasonably innocent patches to the xmonad source;

  - make extraction -- extract Haskell code from the Coq
    implementation of the StackSet module, and postprocess it with
    some final shell scripts;

  - make integration -- tries to build the patched xmonad with the
    extracted StackSet module;

  - make quickcheck -- also runs the QuickCheck testsuite on the
    resulting xmonad binary;

  - make theorems -- gives some indication of how many QuickCheck
    properties have been formalized.

The Coq code is in the src/ directory. Most of the Coq code is in the
StackSet.v module. The Extraction.v module has various extraction
commands to generate somewhat palatable Haskell code. Several
QuickCheck properties have alread been proven in the Properties.v file.

The necessary shell scripts and patches are all in the scripts/ directory.


Author:

	Wouter Swierstra