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 be used to simplify 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 F ! , with a proof component. By enriching the (functional) signature of objects with a specification, the methods and their correctness proofs are packed together in the 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. In particular, we have verified a small hier..