A Type-Based Approach to Divide-And-Conquer Recursion in Coq

Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J Garret Morris, and Aaron Stump

abstract

This paper proposes a new approach to writing and verifying divide-and-conquer programs in Coq. Using ideas from advanced lambda-encodings, combinators are derived in Coq for divide-and-conquer recursion: from outer recursions, one may initiate inner recursions that can construct data upon which the outer recursions may legally recurse. Termination is enforced by the type system of Coq, using just the types of the Calculus of Constructions. In particular, the method does not rely on Coq's native structural recursion. The method is demonstrated on several examples, including mergesort, quicksort, Harper's regular-expression matcher, and others. An indexed version is also derived, implementing divide-and-conquer induction.