Proof Infrastructure for HOL
Proof Infrastructure for HOL
I worked with Wai Wong on the HOL theory of lists. It makes heavy use of the
higherorder fold functions. Conversions for automatically proving theorems
about list operators are provided.
Proof Maintenance
I have examined the problems of maintaining large proof scripts, and
implemented tools to ease some of the problems.
Publications
 Virtual Theories

Paul Curzon. Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications,
eds E. Thomas Schubert, Phillip J. Windley and James AlvesFoss, Lecture Notes in Computer Science 971, pp 138153, SpringerVerlag, 1995.
 The Importance of Proof Maintenance and Reengineering

Paul Curzon. International Workshop on Higher Order Logic Theorem Proving
and Its Applications: BTrack: Short Presentations,
editor Jim AlvesFoss, pp 1732, 1995.
 A Theory of Lists for HOL Based on HigherOrder Functions

Paul Curzon and Wai Wong. In Supplementary Proceedings of the 7th International Workshop on
Higher Order Logic Theorem Proving and its Applications , eds Tom Melham and Juanito Camilleri,
1994.
A Theory of Lists for HOL Based on HigherOrder Functions
Paul Curzon and Wai Wong. Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, eds Tom Melham and Juanito Camilleri, 1994.
Abstract
We describe the new HOL theory of lists. A notable feature is that
it is based largely on higherorder functions: `fold left' and `fold
right'. By using general theorems about these functions we have been able
to provide tools which can quickly prove theorems about both system
and userdefined list constants avoiding the need of induction.
Obtaining the paper
An online version of this paper is here.
The poster presented at the conference is here.
Bibtex Entry
@InProceedings{CurzonWong94HUG,
author = "Paul Curzon and Wai Wong",
title = "A Theory of Lists for HOL Based on HigherOrder Functions",
editor = "Tom Melham and Juanito Camilleri",
booktitle = "Supplementary Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications",
year = "1994",
}
The Importance of Proof Maintenance and Reengineering
Paul Curzon. International Workshop on Higher Order Logic Theorem Proving
and Its Applications: BTrack: Short Presentations,
editor Jim AlvesFoss, pp 1732, 1995.
Abstract
Our work on the verification of real hardware designs using HOL has resulted
in very large proof scripts. Consequently, problems are encountered that are
not an issue in smaller verification efforts. In particular, we have found
that the maintainability of proofs is of paramount importance. There are many
reasons why proof scripts in LCF style theorem provers may be reused. This can
be in order to maintain and understand old proofs as well as to speed the
creation of new ones. Consequently, proofs should be written in styles that
ease their maintainability and make them easier to reuse. Furthermore, proof
tools and interfaces should be designed with proof reuse as well as proof
creation in mind. Many of the problems can be prevented from occurring in the
first place with suitable tool support.
Obtaining the paper
An online version of this paper is here.
Related papers
 Virtual Theories

Bibtex Entry
@InProceedings{Curzon95HUGM,
author = "Paul Curzon",
title = "The Importance of Proof Maintenance and Reengineering",
editor = "Jim AlvesFoss",
pages = "1732",
booktitle = "International Workshop on Higher Order Logic Theorem Proving
and Its Applications: BTrack: Short Presentations",
year = "1995"
}
Virtual Theories
Paul Curzon. Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications,
eds E. Thomas Schubert, Phillip J. Windley and James AlvesFoss, Lecture Notes in Computer Science 971, pp 138153, SpringerVerlag, 1995.
Abstract
We present the notion of virtual HOL theories. These give the effect of
multiple active theories in a HOL session, helping to correct a major deficiency of
the HOL system. They allow the user to switch between different theories at
will, proving theorems and making definitions in each virtual theory in
turn. The system ensures that proofs only use resources available in the
environment of the current virtual theory. The code has
been implemented on top of the HOL90 system. A side effect is that
a version of autoloading is obtained for HOL90. A more radical feature is the
autoloading of tools. The system has been tested on part of a real hardware
verification proof.
Obtaining the paper
An online version of this paper is here.
Related papers
 The Importance of Proof Maintenance and Reengineering

Bibtex Entry
@InProceedings{Curzon95HUGV,
author = "Paul Curzon",
title = "Virtual Theories",
editor = "E. Thomas Schubert and Phillip J. Windley and James AlvesFoss",
volume = "971",
series = "Lecture Notes in Computer Science",
pages = "138153",
booktitle = "Proceedings of the 8th
International Workshop on Higher Order Logic Theorem Proving
and Its Applications",
year = "1995",
publisher = "SpringerVerlag"
}