Hoare-Style Reasoning with (Algebraic) Continuations

Germán Andrés Delbianco     Aleks Nanevski
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 callcc. In this paper 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 working with the logic by verifying a number of characteristic examples.

The ICFP'13 paper can be downloaded from here

The HTTcc source files and examples are availabale from here. You will need to have Coq 8.6 installed, together with the MathComp/SSreflect v. 1.6 libraries.