Inheritance of proofs

The Curry-Howard isomorphism, a fundamental property shared by many type theories, establishes a direct correspondence between programs and proofs. This suggests that the same structuring principles that ease programming should be useful for proving as well. To exploit object-oriented structuring mechanisms for verification, we extend the object-model of Pierce and Turner, based on the higher-order typed λ-calculus with a logical component. By enriching the (functional) signature of objects with a specification, methods and their correctness proofs are packed together in objects. The uniform treatment of methods and proofs gives rise in a natural way to object-oriented proving principles — including inheritance of proofs, late binding of proofs, and encapsulation of proofs — as analogues to object-oriented programming principles. We have used LEGO, a type-theoretic proof checker, to explore the feasibility of this approach.