Program verification is a challenging task. Object-oriented programming languages offer structuring and abstraction mechanisms to support modular design. Main-stream languages support structure their programs in classes, with class-inheritance allowing forms of code reuse and, related to inheritance, subtpying polymorphism offering a flexible form of static typing.
Verification of object-oriented program should, in principle, profit from the mentioned abstraction mechanisms: a clean and modular design is more amendable to be proven correct compared to more low-level representation. Ideally, the structure of the proofs should profit and resemble the structure of the program.
In this thesis, we use calculus of constructions to formalize and verify object-oriented code, exploiting the well-known Curry-Howard isomorphism. We illustrate the approach with verifying properties of a Smalltalk-style collection data types, encoded together with the proof in the theorem prover Lego.