Inheritance of proofs

✍ Scribed by Hofmann, Martin; Naraschewski, Wolfgang; Steffen, Martin; Stroup, Terry

• Publisher: John Wiley and Sons
• Year: 1998
• Tongue: English
• Weight: 176 KB
• Volume: 4
• Category: Article
• ISSN: 1074-3227
• DOI: 10.1002/(sici)1096-9942(1998)4:1<51::aid-tapo4>3.0.co;2-a

✦ Synopsis

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 F ω ≤, 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 typetheoretic proof checker, to explore the feasibility of this approach.