Loading...
Please wait, while we are loading the content...
Similar Documents
Java programs Specifications Coq codes Coq codes
| Content Provider | Semantic Scholar |
|---|---|
| Author | Han, Seokhyun |
| Copyright Year | 2010 |
| Abstract | 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. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://www.cs.rhul.ac.uk/~seokhyun/CEEC2010.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |