containers

This directory contains the Coq representation of Haskell's containers library, as well as our specifications and proofs.

Our ICFP'18 paper "Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)" and its extended version describe the verification of the this library.

The most important components of this work are in the lib and theories directories:

• lib contains the pre-translated Coq representation of Haskell's containers library.
• theories contains our specifications and proofs for containers library. A more detailed documentation about it can be found here.

You can compile the files of the above two directories by running the boot.sh script in this directory (which will invoke Make for these two directories, as well as for their dependencies). You do not need to compile the hs-to-coq tool for this, but you will need Coq 8.8.1 and the ssreflect plugin.

You can regenerate files in the lib directory yourself by running make clean; make from this directory (you will need to compile the hs-to-coq tool for doing that, for detailed instructions check here), or by running the boot.sh in the examples directory.

Other notable components in this directories are:

• the edits file and the module-edits directory (organized in the same structure as the lib directory) record all the edits we make for the translation.
• manual contains all the manually translated modules,
• hs-spec contains all the properties we translated from Haskell's QuickCheck properties, and
• extraction contains the extraction of our translation back to Haskell.