Thoughts about Final Project in AdvHaskell

1. Implement abstract interpretation libraries in Haskell.

   a. There is one binding for PPL library in Haskell:
          http://www.ncc.up.pt/~pbv/research/ppl/ghc.html

   b. I would like to see whether Libapron and the tropical polyhedron library can be possible to implemented in Haskell.

   c. Importance: making Haskell eligible to do numerical static analysis for those compilers written in Haskell.

   d. Compiler.HOOPL package


2. Coq extraction to Haskell.

   a. A way to writing certified Haskell programs.

   b. Whether it's possible to hack in the Extraction component in Coq.

   c. comparing Haskell with Ocaml on coping with Coq Extraction.

   d. Adam Chlipala talks about some concepts about Generic Programming concerning Coq and Haskell:
                http://adam.chlipala.net/cpdt/html/Generic.html
          which might be helpful.

   e. This blog post talks about the Maybe monad emulated with properties proved in Coq:
               http://pdp7.org/blog/?p=100