This project is the outcome of my final master's degree research project. My research involved designing and implementing a verification system for Haskell bytecode (specificly the Yhc bytecode set). Verification is a typechecking analysis on compiled bytecode programs.

Two main products emerged from this research. First, the project final report, which contains a wealth of technical details about the design of the verification system. Second, I wrote a proof-of-concept bytecode compiler and verifier. The code for this compiler is available from this page.

Currently, this compiler is not a full Haskell compiler, as it compiles a specificly designed variant of System F. However, it serves to illustrate the concepts, and the intermediate language it compiles is designed to faithfully represent the Haskell source language, much the why GHC uses a variant of System F during its compilation pipeline. In fact, it may well be possible to use the GHC front-end to generate the IL required by my certifying bytecode compiler. I hope to explore this possibility in the future.

The prototype compiler is available under the GPLv2. See the LICENSE file for details.

The following releases are avaliable for download:

The latest code is avaliable from the darcs repository. The following command will fetch the current code repository to your computer:

  darcs get --partial
     http://www.eecs.tufts.edu/~rdocki01/yhc-cert/