CAO Compiler

Latest on Hackage:0.1.1

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow to host generated Haddocks.

GPL licensed by Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
Maintained by Paulo Silva

CAO Compiler

0. Dependencies
To build the CAO Compiler you need:
- happy
- alex
- cabal package manager

We recommend the installation of the Haskell Platform which contains all the aforementioned dependencies:

1. Build instructions
$ cabal configure
$ cabal build
$ cabal install

2. Run dependencies (optional)
To run the CAO Compiler you may need:
- Yices SMT solver (version 1)

This SMT solver is used to check some more complex conditions when typechecking a CAO program.
The compiler works without Yices but some conditions may not be verified. A warning is shown in these cases.

3. Backend library dependencies
To compile the generated code with the backend library you need:
- GMP (optional)

NTL is available from
GMP is available from

Information about how to compile NTL with GMP can be found here:

4. Run instructions
To see a description of all compiler options:
$ cao help

The basic compiler usage is:
$ cao comp [cao-file]

5. Example
In the 'example' directory you can find a CAO implementation of the SHA1 hash algorithm.
The Makefile provides an example of how a generated C program can be compiled and linked with the backend library.
You may have to adjust the script variable 'CAO_PATH' to the root directory of your installation.

Contact Information

Bugs/Suggestions please mail to:

Manuel Barbosa -
Paulo Silva -


B�bara Vieira -
David Castro -
H�der Pereira -
Manuel Barbosa -
Miguel Marques -
Nuno Rodrigues -
Paulo Silva -
Tiago Oliveira -
comments powered byDisqus