Hoare-Style Reasoning with (Algebraic) Continuations

Continuations are programming abstractions that allow for manip-ulating the “future ” of a computation. Amongst their many ap-plications, they enable implementing unstructured program flow through higher-order control operators such as callcc. In this pa-per we develop a Hoare-style logic for the verification of programs with higher-order control, in the presence of 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 types. Our operators are algebraic in the sense of Plotkin and Power, and Jaskelioff, to reduce the annotation burden and enable verification by symbolic evaluation. We illustrate work-ing with the logic by verifying a number of characteristic examples