Quickstart

Coma (which stands for Continuation Machine) is an Intermediate Verification Language implemented as a plugin in 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.