We present an implementation of a program logic of objects, extending that (AL) of Abadi and Leino. In particular, the implementation uses higher-order abstract syntax (HOAS) and—unlike previous approaches using HOAS—at the same time uses the built-in higher-order logic of the theorem prover to formulate specifications. We give examples of verifications, extending those given in [1], that have been attempted with the implementation. Due to the mixing of HOAS and built-in logic the soundness of the encoding is nontrivial. In particular, unlike in other HOAS encodings of program logics, it is not possible to directly reduce normal proofs in the higher-order system to proofs in the first-order object logic.
CITATION STYLE
Hofmann, M., & Tang, F. (2000). Implementing a program logic of objects in a higher-order logic theorem prover. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1869, pp. 268–282). Springer Verlag. https://doi.org/10.1007/3-540-44659-1_17
Mendeley helps you to discover research relevant for your work.