Informatics Report Series


Report   

EDI-INF-RR-0033


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:A Higher-Order Embedding of a Logic of Objects
Authors: Martin Hofmann ; Francis Tang
Date:Jan 2001
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh