Coma: an intermediate verification language with explicit abstraction barriers

Coma is a formally defined intermediate verification language. It adopts the continuation-passing style which allows us to express in a natural manner the standard control structures—conditionals, loops, subroutine calls, and exception handling—using only three elementary constructions.
A special programming construct representing the abstraction barrier allows the programmer to decide which part of a function implementation is visible to (and verified by) the caller, and which part is hidden from the caller and verified at the definition site. This offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths.

Paper presented at ESOP 2025: https://doi.org/10.1007/978-3-031-91121-7_8