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

• To: types@cis.upenn.edu
• Subject: Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover
• From: Francis Tang <fhlt@dcs.ed.ac.uk>
• Date: Fri, 3 Mar 2000 11:47:28 +0000 (GMT)
• cc: Martin Hofmann <mxh@dcs.ed.ac.uk>, Francis Tang <francis.tang@dcs.ed.ac.uk>

Dear all,

I would like to draw your attention to the following preprint
available from http://www.dcs.ed.ac.uk/home/fhlt/Research/

Comments and suggestions are very welcome!

Yours faithfully,

Francis.


Implementing a Program Logic of Objects in a Higher-Order Logic Theorem
Prover
 
          by Martin Hofmann and Francis Tang

We present an implementation of a program logic of objects, extending that
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 and is
established by way of a semantic interpretation based on ideas from
category theory. The details of this interpretation will be given
elsewhere.

--
Francis Tang                       Email: francis.tang@dcs.ed.ac.uk
LFCS, Division of Informatics,     Url: http://www.dcs.ed.ac.uk/~fhlt/
University of Edinburgh,           Office: Rm 1603, JCMB, KB
Edinburgh  EH9 3JZ, Scotland.      Tel: +44 131 650 5185

• Prev: Haskell Workshop
• Next: 7th WoLLIC'2000
• Index(es):
  • Main
  • Thread