Basic Hoare logic, without recursive procedures, admits proofs of correctness that are linear in the size of the program under consideration. This is why proof outlines, which annotate programs with assertions that must hold of intermediate states, are so useful. In this talk, we discuss how to reason about programs which have recursive procedures, and how one traditionally verifies their correctness: using proofs that are quadratic in the size of the program. But, in case of call-by-value parameter passing, we can implode proofs by introducing new proof rules, "contracts," and a beautiful proof normalization procedure, leading again to proofs linear in the size of the program!

Collaborators: Krzysztof Apt, Frank de Boer