- Abstract:
-
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. Instead, we prove soundness directly by first giving an interpretation the higher-order logic.
- Copyright:
- 2001 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @Misc{EDI-INF-RR-0033,
- author = {
Martin Hofmann
and Francis Tang
},
- title = {A Higher-Order Embedding of a Logic of Objects},
- year = 2001,
- month = {Jan},
- }
|