Continuations are programming abstractions that allow for manipulating the “future” of a computation. Amongst their many applications, they enable implementing unstructured program flow through higher-order control operators such as the callcc operator of your functional programming language of choice.

In this talk we present HTTcc, a Hoare-style logic for the verification of programs with higher-order control, in the presence of mutable dynamic state. This is done by designing a dependent type theory with first class callcc and abort operators, where pre- and postconditions of programs are tracked through dependent types. Our operators are algebraic in the sense of Plotkin and Power, to reduce the annotation burden and enable verification by symbolic evaluation.

As a roadmap for this talk, we illustrate working with HTTcc by means of the verification of a couple of non-trivial examples.