Markus Aderhold. Second-Order Programs with Preconditions. In Simon Siegler, Nathan Wasser, editors, Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday. Volume 6463 of Lecture Notes in Computer Science, pages 129-143, Springer, 2010. [doi]