Martin Hofmann and Francis Tang (2000)

# Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover

In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, ed. by Mark Aagaard and John Harrison, vol. 1869, pp. 268-282, Springer. Lecture Notes in Computer Science (ISBN: 3-540-67863-8).

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.

Document Actions