Some background on the materials.
Methodological themes.
HOL and ProofPower
Foundational Studies
Some background on the materials.
The Subject Matters

This page provides links to a variety of materials which are of largely historical interest, and concern primarily my work for International Computers Limited during the years 1986-1995. Whether these have interest to anyone but myself is moot. For myself, it sometimes handy to be able to refer back to these materials.

I will also include links to more recent materials which show the later development of the themes addressed during this period.

The State of the Materials

The documents acessible through these pages were prepared during a period in which the technology used for preparing documents was evolving and generally involved both open source software and our own adaptations (primary for the purpose of presenting logical and mathematical material in a form which would be processable by various software tools).

I do not now have the means to present these documents correctly, though from time to time I spend a bit more effort on the task of re-engineering the presentation of the documents, and as I do this the documents as accessed here move closer to the originals. The principal symptom of this malaise at present is in the mathematical and logical symbols, which in many of the documents are not correctly presented, but in some cases other pathologies appear.

Another factor limiting the available materials arises from the fact that we were sometimes working on classified materials. Consequently when I came away I had to select a subset of the documents excluding any which contained sensitive material. I have little memory of this selection process, but since I do have a kind of index which mentions documents which I no longer have, I can see that I discarded not only those containing sensitive materials, but also some which I presumably considered of no enduring interest.

If anyone should find a document to be of interest which does not appear to be correctly presented then they should contact me and I will see whether I can move things forward to improve the presentation of the material of interest to them (though by this I mean the process of rendering the original source e.g. getting the characters printed correctly, rather than addressing the defects in the original).

Methodological themes.
Introduction and Background
General Themes
The Z Specification Language
The Language
Semantics and Proof
Z in HOL
ProofPower and Z in HOL
The VDM Specification Language
A (rather insignificant) contribution to the development of the standard for the VDM specification language.
I was quite briefly involved in the VDM standardisation effort, serving as secretary to the panel in lieu of John Dawes who was much better suited to the position but had been taken from this role by management fiat. I did take all the minutes, probably not as well as John would have done, but I also tried to influence the standard by putting "proof theory" on the agenda and putting forward ideas about the semantics intended to make for a proof theoretically strong deductive system. Most signficantly, for me, I diverted my foundational research to the problem, common to Z and VDM of how to do foundation systems in a well-founded ontology which supported both polymorphism and modular specification. This foundational work appears under the "Foundations" heading below, not here.
My explorations in the foundations of mathematics.
Well-Founded Ontologies
Non-Well-Founded Ontologies
Specifications in SML
I rather liked using functional programming languages for writing small "formal" specifications of various things to do with languages (abstract syntax, deductive systems).
Miscellaneous Presentations
Typically for progress meetings or external presentations of our formal methods work.

up quick index © RBJ

privacy policy


$Id: index.xml,v 1.2 2012/06/29 21:42:53 rbj Exp $