Coma language

Top level declarations in Coma files can be of two kinds:

• Logical declarations introduce data types, logical functions and predicates, as well as axioms and lemmas. These declarations are used to specify the Coma programs. Their syntax and semantics are precisely those of WhyML.
• Program declarations introduce Coma handlers which perform stateful computations and whose correctness we prove when we verify a Coma program.