Working with HOL

Overview:

I was first acquainted with Higher Order Logic and the HOL proof tool when I joined the ICL Defence Systems Formal Methods Group in January 1986. Since then I have done a variety of small bits of work on or with HOL.
security: I have written security models and participated in the formal verification of secure systems using both Z and HOL
hardware verification: I lead the formal verification of the "One Way Regulator", a UKL6 certified commercial product.
foundations: I did some work on alternatives to ZF, using "ZF-HOL", an axiomatisation of ZFC in Classic HOL.
Z in HOL: I was the prime mover in the ICL work exploiting HOL as a proof tool for Z, and designed the semantic embedding of Z into HOL used by ProofPower.
ProofPower: I conceived and lead the "FST" project, a collaboration between ICL, PVL, Cambridge and Kent Universities under which ICL developed ProofPower, an implementation of HOL supporting proof in Z.
now: I'm looking at Richard Boulton's "Claret" with a view to doing some work on the semantics of Verilog and possibly other hardware description languages. I'm also ruminating about how to implement HOST.
future: My fantasies about The Global SuperBrain involve Higher Order Set Theory as a foundation. This is my line on a future for HOL. I'd also like to do a bit more on "foundations" with HOL.

Security:

I have written security models and participated in the formal verification of secure systems using both Z and HOL.

first model: in 1986 I wrote my first formal security model, for GCHQ, in Z and transcribed it into HOL for proof work. This was the start of our work on Z in HOL. In 1987 Kevin Blackburn took over the detailed work both on the security proofs and support for Z in HOL, and we jointly wrote a paper (unpublished) entitled "Translating Z into HOL".
Relational Databases: I contributed to the early stages of a contract with RSRE concerning formal treatment of their secure relational database SWORD, by producing a formalisation of the security requirement, and identifying a way of structuring the formal semantics of the query language so that a security proof would be tractable. Specifications in HOL, proofs completed (by Gill Prout and Rob Arthan) using ProofPower.
OWR: I was the "architect" of the formal verification of the security of the One Way Regulator, and lead the formal methods team which did all the real work. see hardware verification.

Hardware Verification:

I lead the formal verification of the "One Way Regulator", a UKL6 certified commercial product.
methods: The OWR was specified in HOL with transcripts supplied in Z. It was a hardware device, designed by ICL to meet the security requirement. The design was formally proven against the security requirement using a specially modified version of Classic HOL. This involved formal reasoning about information flow bandwidths.
modifying HOL: HOL was modified, to make it more secure, and to permit loose constant specifications. "new_axiom" and "mk_thm" were hidden from users. Loose specifications were enabled by permitting the deletion of definitions, using a definition using the choice function, deriving a theorem of the form "existsx.P x turnstile P c" and then deleting the definition.
reals: We had a look at implementing reals in HOL (this was 1988), using represention of real numbers as open downward-closed cuts in pre-rationals represented as triples of natural numbers ((a,b,c) represents the rational ((a-b)/(c+1)). This was pretty heavy going (no linear arithmetic). Long before we had the reals we had a way of talking about bandwidth without them, so we had to give up that little project and get on with the real work.

Foundations:

I did some research on alternatives to ZF, using "ZF-HOL", an axiomatisation of ZFC in Classic HOL.
Motive: I was working on the VDM standard, and had this idea that specification languages should be as expressive as mathematical foundation systems, so I wanted to come up with a semantic foundation suitable for a VDM which met that criterion.
Criteria: So I wanted a foundation system which was (a) well founded (b) as rich as ZFC (c) based on functions not sets (d) polymorphic functions (e) supported modularity. Also I wanted the theory of functions to be both pure and extensional.
Method: The idea is to start from a suitable semantic domain, define appropriate operators over the domain, establish by proof properties of these operators which would form the basis for the axiomatisation of the logic of the specification language. To do this in HOL and end up with a specification language of the same strength as ZFC is not possible without first extending HOL, which can be done by introducing a new type which made into a model for ZFC by appropriate axioms. HOL thus extended I called ZF-HOL. Using this type as raw material the required semantic domains can be constructed.
pure functions are obtained by filtering the sets yeilding a collection of functions as large as the universe of ZFC.
polymorphic pure functions are pure functions parameterised by assignments of values to type variables (the assignments also represented by pure functions).
structured polymorphic pure functions are one step higher intended to support local definitions and modules.
pure categories I also tried a foundation system in which everything is a category, just out of curiosity. It didn't work, but one day I'd like another crack at it.

ProofPower:

I conceived and lead the "FST" project, a collaboration between ICL, PVL, Cambridge and Kent Universities under which ICL developed ProofPower, an implementation of HOL supporting proof in Z.
purpose: we wanted a good proof tool for formal methods work which had to be able to work with Z specifications. It wasn't clear that Z would be tractible for proof, the proof rules were not understood. So cutting our teeth on re-engineering HOL and doing the best achievable proof support for Z on that base seemed a good idea.
the project: We put together a collaboration to bid for support from the DTI under its "IED" initiative. The members in the end were ICL, Program Validation Limited, The University of Cambridge (foundational research under Martin Hyland) and the University of Kent (Keith Hanna and Veritas). The project was called "Foundations and Tools for Formal Verification", and ICL's part of this project was the implementation of what was later called ProofPower, a re-engineered HOL.
results: We re-implemented HOL twice (the first was a test run) and embedded the Z specification language into HOL. The result was christened ProofPower, and became a commercial product (though that wasn't the original intention). Later support for the DERA compliance notation was implemented, enabling verification of SPARK programs against Z specifications.

Z in HOL:

I was the prime mover in the ICL work exploiting HOL as a proof tool for Z, and designed the semantic embedding of Z used by ProofPower.
first steps: we started off in 1986 by manually transcribing Z specifications into HOL and gradually built up ad hoc methods and tools for working in this way. This included libraries to support the kinds of data structures found in Z and to match the Z library, techniques for working with Z like schemas and axiomatic specifications in a rigorous and conservative way, and also tools which allowed HOL specs to look more like the Z specs they were based on (extended character set, and Z-like boxes).
the embedding: in 1990, with a prototype ICL-HOL in the bag, I though about Z in HOL and figured out how to do a full and faithful embedding. I specified the mapping in Z and a prototype was produced on the prototype ICL-HOL The trickyest problems were probably the handling of bound variables (Z has some really exotic variable binding constructs), and the support of Z's novel set generic polymorphism.
implementation: ProofPower Z was then implemented on the "product quality" implementation of ICL-HOL (later christened ProofPower). The work on Z contributed to some of the novel features of ProofPower, for example, the multi-lingual quotation mechanisms, and the context sensitive proof automation which permitted features like "strip_tac" to change behaviour radically when reasoning in Z to the way it behaves for HOL (e.g. understanding schema conjunction as well as logical conjunction).

Now:

I'm looking at Richard Boulton's "Claret" with a view to doing some work on the semantics of Verilog and possibly other hardware description languages. I'm also ruminating about how to implement HOST.
Claret: is a tool to support semantic embedding of languages into HOL. It takes a file describing the syntax of the language are generates a parser, a pretty printer, parse tree datatypes in standard ML and in HOL. Even if you don't want to do the embedding these can be handy for defining the semantics of the language or for prototype implementations.
HOST: is Higher Order Set Theory, (to be) implemented as an LCF-like proof system with the compiler built into the logical kernel, compiling executable function definitions to give fast evaluation during rewriting. This means (in theory) that semantic embedding yields efficient simulators.
SML and Verilog: I need a semantics in HOL for a subset of SML to do an embedding which legitimises integration of an SML compiler into the HOST kernel. The semantics of verilog is then a target application for the HOST system. Embedding verilog (or some other Hardware Description Language) yeilds both a tool for reasoning about harware and an efficient simulator.

Future:

My fantasies about The Global SuperBrain involve Higher Order Set Theory as a foundation. This is my line on a future for HOL. I'd also like to do a bit more on "foundations" with HOL.
the Global SuperBrain: under this extravagent rubrick I am thinking about how to do distributed logicist AI. For this purpose I believe one needs a foundation system adequate for modern mathematics and know none which seems to me more practical than Higher Order Set Theory.
the megakernel: to support the AI angle the LCF paradigm must be bludgeoned into delivering higher performance, particularly when evaluating functions defined in the foundational logic (or in languages embedded in that logic). For this purpose I seek an embedding of a practical functional language into the logic, the compiler for which would then be integrated into the logical kernel.
other foundational work: I would also like to have another crack at the theory of pure functions and a theory of pure categories, defined and explored using ZFC in HOL. This is just entertainment, I don't expect it to be useful, so that means it may never happen (though that doesn't distinguish it from much around here!).


UP HOME © RBJ created 1998/06/04 modified 1998/06/30