Termination of Open Higher-Order Programs

We study the problem of proving termination of open, higher-order programs with recursive functions and datatypes. We identify a new point in the design space of solutions, with an appealing trade-off between simplicity of specification, modularity, and amenability to automation. Specifically, we consider termination of open expressions in the presence of higher-order, recursive functions, and introduce a new notion of termination that is conditioned on the termination of the callbacks made by the expressions. For closed expressions our definition coincides with the traditional definition of termination. We derive sound proof obligations for establishing termination modulo callbacks, and develop a modular approach for verifying the obligations. Our approach is novel in three aspects. (a) It allows users to express properties about the environment in the form of higher-order contracts. (b) It establishes properties on the creation sites of closures instead of application sites and does not require knowing the targets of applications. (c) It uses a modular reasoning where termination (modulo callbacks) is verified for each function independently and then composed to check termination of their callers. We present the results of evaluating our approach on benchmarks comprising more than 10K lines of functional Scala code. The results show that our approach, when combined with a safety verifier, established both termination and safety of complex algorithms and data structures that are beyond the reach of state-of-the-art techniques. For example, it verifies Okasaki's scheduling-based data structures and lazy trees in under a few seconds.