Quickstart

Coma (continuation machine) is an Intermediate Verification Language on top of the Why3 platform.

Continuation-passing style allows us to devise an extremely economical abstract syntax for a generic verification language. This syntax is flexible enough to naturally express conditionals, loops, (higher-order) function calls, and exception handling. It is type-agnostic and state-agnostic, which means that we can combine it with a wide range of type and effect systems.

Shiele — Four Trees

Shiele — Four Trees