Name
Abstract | ||
|---|---|---|
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 X-calculus F less than or equal to(omega), 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. (C) 1998 John Wiley & Sons, Inc. |
Year | DOI | Venue |
|---|---|---|
1998 | 3.0.CO;2-A" target="_self" class="small-link-text"10.1002/(SICI)1096-9942(1998)4:13.0.CO;2-A | TAPOS |
Field | DocType | Volume |
Programming language,Computer science,Mathematical proof,Distributed computing | Journal | 4 |
Issue | ISSN | Citations |
1 | 1074-3227 | 4 |
PageRank | References | Authors |
0.79 | 1 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Martin Hofmann | 1 | 145 | 23.77 |
| Wolfgang Naraschewski | 2 | 57 | 7.89 |
| Martin Steffen | 3 | 122 | 10.32 |
| Terry Stroup | 4 | 15 | 2.38 |