Skip to content


Subversion checkout URL

You can clone with
Download ZIP


Put optimisation off by default, bump to 0.2


Add inliner and use it when translating contracts
The inliner inlines non-recursive, non-casing functions, when inlining
the function would not insert a new lambda.  When dealing with
contracts, it allows inserting a lambda after the :-> because it uses
higher-order abstract syntax.

The inliner can be debugged with --db-inliner and --dump-inlined-core.
A new flag --db-names gives some debug information about all top level
variables in the program.

By using the inliner, we can now without hassle use GHC's
optimiser. It is now on by default. It chops up contracts into several
top-level functions, but the inliner then restores the structure by
making it one big definition. Before, the translator would carry around
a context and buggily inline sometimes, but now this is separated.

When using optimisation, we also get rid of the nasty bug when an expression
is cased on twice, with default branches. Without optimisation, you can get
unsoundness with functions pattern-matching on two arguments.

A scratch on parameterised contracts is added as a side effect, but it's not
well tested yet.

Statements can now depend on both data types and functions.


The state the article and the tool was when submitting to POPL


Add raw results from the big test suite run
Something went wrong with that request. Please try again.