zbMATH — the first resource for mathematics

Implementing a program logic of objects in a higher-order logic theorem prover. (English) Zbl 0974.68185
Aagaard, Mark (ed.) et al., Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14-18, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1869, 268-282 (2000).
Summary: 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 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.
For the entire collection see [Zbl 0944.00036].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)