Verification of Java programs in Coq

This paper is a research on functional interpretation of object-oriented programs in the intensional type theory with dependent record types and coercive subtyping. We are here simulating a type-theoretic model of Java programs in Coq. Representing a class and its interface-type, which declares a set of methods and their signatures for code reuse, as dependent record types, the type-theoretic encoding enjoys desirable subtyping relationships that correctly capture the important object-oriented features such as inheritance, subtype polymorphism and dynamic dispatch. Furthermore, since the model is given in the intensional type theory, machine-supported verification of Java programs can be done by proving specifications that is satisfied by Java programs in Coq with regard to the state of objects.