Automated Reasoning Group Old FTP Area for HOL

University of Cambridge Computer Laboratory This page provides information about various old releases of HOL.
For the latest release see the current FTP page.

Lab | ARG | Description | HOL | Isabelle | Members | Haiku


The Cambridge FTP Area for HOL


This is a guide to the anonymous ftp area for the HOL System at the University of Cambridge Computer Laboratory. There is a README file. You may access the ftp directory directly or follow the hyperlinks below to find what you are looking for. The GNU compression utility, gzip, is provided here for your convenience.

The users of HOL in Cambridge are part of the Automated Reasoning Group.


In case of difficulty send electronic mail to hol-support@cl.cam.ac.uk.

Hol98 Source Code


The Hol98 version of
the HOL System is available here. Athabasca, version 2 is the latest supported release. To build it you will need the source for MoscowML version 1.43.


Back to index for the Cambridge FTP Area for HOL
In case of difficulty send electronic mail to hol-support@cl.cam.ac.uk.

HOL90 Source Code


The HOL90 version of
the HOL System is available here. Version 10 is the latest supported release. To build it you will need Standard ML of New Jersey version 110.

Version 7 is the previous supported release. To build it you will need Standard ML of New Jersey version 0.93.

You will need the GNU compression utility to unpack the files.

Information on building HOL90 for various architectures may be found by browsing the archive of the info-hol mailing list.

If you are outside Europe, there are other HOL sites.


Back to index for the Cambridge FTP Area for HOL
In case of difficulty send electronic mail to hol-support@cl.cam.ac.uk.

HOL88 Source Code and Manuals


The HOL88 version of
the HOL System is available here. The sources and documentation are in separate gzipped tar files. Read the release note for the latest version. The supported libraries are included in the sources. The contributed libraries are available separately.

You will need the GNU compression utility to unpack the files and GNU Common Lisp (GCL) to build them. (Some other versions of Lisp may also work.) GCL used to be called Austin Kyoto Common Lisp (AKCL).

A tried-and-tested Lisp for building HOL88 on Sun machines under SunOs is AKCL version 1.605. To build AKCL you will also need the KCL tar file. There is a modified version of the KCL tar file for the MIPS architecture. See the README file for how to build AKCL.

Information on building HOL88 for other architectures may be found by browsing the archive of the info-hol mailing list.

If you are outside Europe, there are other HOL sites.


Back to index for the Cambridge FTP Area for HOL
In case of difficulty send electronic mail to hol-support@cl.cam.ac.uk.

Contributed Libraries for HOL88


Listed below are the contributed libraries for the HOL88 version of
the HOL System. The sources, documentation and supported libraries of HOL88 can be found here. The contrib directories are available as tar files. You will need the GNU compression utility to unpack these.

The contrib directory contains contributions from the HOL user community. They are not edited, and the University of Cambridge Computer Laboratory assumes no responsibility to support any code or tools distributed in the directory.

The aim of contrib is to provide a vehicle to make it easy for the HOL community to share theories, proofs, examples, tools, documents, and other material which may be of interest to users of the HOL system, but which is not included in the library.

Each contribution is given a separate subdirectory within contrib. A standard READ-ME file is included in each subdirectory, giving at least the following information:

Contributors may also include other information in the READ-ME file.


ind-defs by John Harrison (95.05.08) [New]
Mutually inductive definitions with arbitrary monotone hypotheses

TkHolWorkbench by Donald Syme (95.04.04) [New]
Interface for HOL implemented using the Tk toolkit

cpo by Wishnu Prasetya (94.06.01) [New]
Theory of CPOs and lattices

DerLem by Wishnu Prasetya (94.03.23) [New]
Enhancements to subgoal package for equational and forward proof

pre-v2.02-rewr by Richard Boulton (94.02.18)
Compatibility files for the rewriting in HOL88.2.02

RefCalc by Joakim von Wright (94.02.09)
Program verification and refinement in predicate transformer semantics

Z by Mike Gordon (94.01.24)
Shallow embedding of Z in HOL

HOLproof by Joakim von Wright (93.09.24)
A formalisation of higher order logic proofs in HOL

sml-mode by Wai Wong (93.09.16)
SML mode for gnuemacs Version 19.XX

greatest by Catia Angelo (93.06.04)
Theory about the greatest of a list of natural numbers etc

reduct by John Harrison (93.05.31)
reflexive/symmetric/transitive closure; abstract reduction relations

AKCL-profiling by John Van Tassel (93.05.14)
Rudimentary profiling utility for AKCL

rec_tys_listop by Brian Graham (93.05.07)
An extension to the types which can be automatically defined

Predicate by Wishnu Prasetya (93.04.05)
Theory of lifted predicates in HOL

mweb by Wishnu Prasetya (93.04.02)
The mweb suite of source documentation and management utilities.

int by John Harrison (93.03.04)
Integers theory

WF by Wishnu Prasetya (92.12.04)
Theory of well founded relations

AKCL-mods by John Van Tassel (92.12.01)
A hol-init file to increase the speed of HOL when built under AKCL

make_use by Donald Syme (92.11.25)
Automatically generates autoloading commands for a theory

prog_logic92 by Gavan Tredoux (92.11.04)
Program semantics inc. (unbounded) nondeterminism, total correctness

newrw by Jim Grundy (92.10.??)
Updates rewriting conversions in HOL2.0 code to HOL2.01

Tarski by Flemming Andersen & Kim Dam Petersen (92.10.29)
Definition of a theory for defining recursive boolean functions

smarttacs by Donald Syme (92.10.25)
Several general purpose tactics

fpf by Donald Syme (92.10.25)
A theory of finite partial functions (finite maps)

boyer-moore by Richard Boulton (92.10.16)
Boyer-Moore Automation for HOL

hol-exec by Sreeranga Rajan (92.10.07)
HOLER: The HOL Evaluator

pred by Ching-Tsun Chou (92.10.06)
A Sequent Formulation of a Logic of Predicates in HOL

cont by Ching-Tsun Chou (92.10.06)
Interactive Theorem Proving with Theorem Continuation Functions

aci by Ching-Tsun Chou (92.10.06)
Generalizing AC operation with identity to finite sets

hol-sum by Wai Wong (92.09.18)
Summary of HOL system Version 2

rule-induction by Juanito Camilleri & Tom Melham (92.09.01)
Examples using the inductive definitions package

res_quan by Wai Wong (92.08.??)
Library for dealing with restricted quantifiers

Xhelp by Sara Kalvala (92.08.26)
Xwindows browser for HOL documentation

non-unix by John Carroll (92.06.18)
Instructions for making HOL on non-UNIX machines

holsort by Steve Brackin (92.03.02)
Sorts files of axioms, etc., or of typed constants

SECD by Brian Graham (92.02.27)
The SECD microprocessor specification and verification

koenig by Paul Loewenstein (91.08.??)
A proof of Koenig's Lemma

prooftree by Sara Kalvala (91.08.21)
Enhanced subgoal package

UNITY by Flemming Andersen (91.02.07)
Definition of the UNITY theory, described by Chandy and Misra

convert by David Shepherd (91.02.01)
Various conversion orientated stuff

hol-emacs by Phil Windley (91.01.??)
A simple interface for running HOL under the GNU Emacs editor

benchmark by Mike Gordon (91.01.28)
The HOL "multiplier" benchmark (for version 1.12)

tex-thy-format by Wai Wong (91.01.27)
Format a HOL theory in LaTeX format

mut_rec_types by Peter Strarup Jensen, Ann-Grete Tan & Anders Pilegaard
(91.01.25)
Defining mutually recursive types in HOL

btg-tactics by Brian Graham (91.01.25)
Extra general-purpose tactics

hol_users by Sara Kalvala (91.01.20)
Information on groups using HOL

latex by Jim Alves-Foss (90.12.14)
LaTeX macros for typesetting HOL

subgoal by Roger Fleming (90.12.12)
Experimental new subgoal package

rewriting by Roger Fleming (90.11.14)
Rewriting tools

temporal by Amit Jasuja (90.08.03)
Temporal logic in HOL

CPO by Albert Camilleri (90.06.01)
Basic theory of CPO's and fixed-points

select by Brian Graham (90.04.20)
Note on dealing with the epsilon-operator in HOL proofs

tooltool by David Shepherd (90.04.11)
SunView HOL interface tool (using tooltool)

knuth-bendix by Konrad Slind (90.04.11)
Knuth Bendix completion as a derived inference rule

franz-cl-th by John Carroll (90.04.11)
Unix script for translating theory files from Franz to common lisp

batch-hol-tool by Richard Boulton (90.04.11)
Batch HOL session with merged input and output

PNF by Clive Jervis (90.04.11)
Conversions to reduce terms to prenex normal form

hol-mode by Kim Dam Petersen (89.??.??)
Emacs HOL (Higher Order Logic) Mode

eval (89.12.29)
lisp-coded conversions and rules for dealing with constants etc.

CSP by Albert Camilleri (89.12.07)
Definition of csp trace theory

CARD by Ton Kalker (89.09.25)
Theory of cardinals via quotient structure

int_mod by Elsa Gunter (89.07.27)
subgroups of the integers and basic modular arithmetic

ZET by Ton Kalker (89.07.10)
Definition of the integers: zet

WELL_ORDER by Ton Kalker (89.07.10)
Proof that every set can be wellordered

bags by Philip Leveilley (89.06.29)
Library "bags" moved to contrib

quotient by Ton Kalker (89.06.08)
Definition of quotient types

auxiliary by Ton Kalker (89.06.08)
Definition of auxiliary theory

fixpoints by Mike Gordon (89.04.03)
Definition of a fixedpoint operator and derivation of Scott Induction

icl-taut by Roger Jones (89.03.30)
Various theorem proving utilities, including a tautology checker

prog_logic88 by Mike Gordon (89.03.23)
Library "prog_logic88" moved to contrib

integer by Elsa Gunter (89.03.23)
Theory of integers

group by Elsa Gunter (89.03.20)
Library "group" moved to contrib

wordn by Wai Wong (Date of inclusion unknown)
Theory of n-bit words

more_lists by Paul Curzon (Date of inclusion unknown)
Library "more_list" moved to contrib

hol-errors by Phil Windley (Date of inclusion unknown)
Interpretations of various HOL errors and how to fix them (sometimes)


Back to index for the Cambridge FTP Area for HOL
In case of difficulty send electronic mail to hol-support@cl.cam.ac.uk.

Technical Reports by the HOL Group in Cambridge


This page contains a list of the
University of Cambridge Computer Laboratory technical reports that relate to the HOL System and are available by ftp. The reports are listed alphabetically by first author, and chronologically for each author. Other Computer Laboratory technical reports are also available. There is a list of papers and theses (some of which appear below as technical reports).
Richard Boulton (rjb@cl.cam.ac.uk), Mike Gordon (mjcg@cl.cam.ac.uk),
John Herbert (herbert@cam.sri.com) and John Van Tassel (jvt@ti.com)
The HOL Verification of ELLA Designs
Technical Report 199, August 1990.
PostScript / Abstract.

Richard J. Boulton (rjb@cl.cam.ac.uk)
On Efficiency in Theorem Provers which Fully Expand Proofs into Primitive Inferences
Technical Report 248, February 1992.
DVI / Abstract.

Richard J. Boulton (rjb@cl.cam.ac.uk)
A HOL Semantics for a Subset of ELLA
Technical Report 254, April 1992.
DVI / Abstract.

Richard John Boulton (rjb@cl.cam.ac.uk)
Efficiency in a Fully-Expansive Theorem Prover
Technical Report 337, May 1994.
DVI / Abstract / Web Page.

Juanito Camilleri (juan@unimt.mt) and Tom Melham (tfm@dcs.gla.ac.uk)
Reasoning with Inductively Defined Relations in the HOL Theorem Prover
Technical Report 265, August 1992.
PostScript.

Victor A. Carreño (vac@air16.larc.nasa.gov)
The Transition Assertions Specification Method
Technical Report 279, January 1993.
PostScript.

Paul Curzon (pc@cl.cam.ac.uk)
Of What Use is a Verified Compiler Specification?
Technical Report 274, November 1992.
PostScript.

Paul Curzon (pc@cl.cam.ac.uk)
A Verified Vista Implementation
Technical Report 311, September 1993.
PostScript.

Paul Curzon (pc@cl.cam.ac.uk)
The Formal Verification of the Fairisle ATM Switching Element: an Overview
Technical Report 328, March 1994.
PostScript.

Paul Curzon (pc@cl.cam.ac.uk)
The Formal Verification of the Fairisle ATM Switching Element
Technical Report 329, March 1994.
PostScript.

Andrew D. Gordon (adg@cl.cam.ac.uk)
A Mechanised Definition of Silage in HOL
Technical Report 287, February 1993.
DVI / Abstract.

Michael J. C. Gordon (mjcg@cl.cam.ac.uk)
Mechanizing Programming Logics in Higher Order Logic
Technical Report 145, September 1988.
DVI.

Jim Grundy (Jim.Grundy@abo.fi)
A Method of Program Refinement
Technical Report 318, November 1993.
PostScript / Abstract / Directory.

Thomas F. Melham (tfm@dcs.gla.ac.uk)
Using Recursive Types to Reason about Hardware in Higher Order Logic
Technical Report 135, May 1988.
DVI / PostScript.

T. F. Melham (tfm@dcs.gla.ac.uk)
A Mechanized Theory of the pi-calculus in HOL
Technical Report 244, January 1992.
PostScript.

Monica Nesi (monica@smaq20.univaq.it)
A Formalization of the Process Algebra CCS in Higher Order Logic
Technical Report 278, December 1992.
PostScript (A4 paper) / PostScript (US paper).

John Peter Van Tassel (jvt@ti.com)
Femto-VHDL: The Semantics of a Subset of VHDL and its Embedding in the HOL Proof Assistant
Technical Report 317, November 1993.
Abstract / Directory.

Wai Wong (wwong@comp.hkbu.edu.hk)
Formal Verification of VIPER's ALU
Technical Report 300, April 1993.
PostScript.

Wai Wong (wwong@comp.hkbu.edu.hk)
Recording HOL Proofs
Technical Report 306, July 1993.
PostScript.


Back to index for the Cambridge FTP Area for HOL
In case of difficulty send electronic mail to hol-support@cl.cam.ac.uk.

Papers and Theses by the HOL Group in Cambridge


This page contains a list of some papers and theses written by members of the
HOL group at the University of Cambridge Computer Laboratory. The documents are listed alphabetically by first author, and chronologically for each author. You may access them directly in the ftp directory. There is also a list of Computer Laboratory technical reports that relate to the HOL System (some of which appear in the list below).
Richard Boulton (rjb@cl.cam.ac.uk), Andrew Gordon (adg@cl.cam.ac.uk),
Mike Gordon (mjcg@cl.cam.ac.uk), John Harrison (jrh@cl.cam.ac.uk),
John Herbert (herbert@cam.sri.com), and John Van Tassel (jvt@ti.com)
Experience with Embedding Hardware Description Languages in HOL
In V. Stavridou, T. F. Melham and R. T. Boute (editors), Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, June 1992, pages 129-156. IFIP Transactions volume A-10, North-Holland/Elsevier.
DVI / PostScript.

Richard John Boulton (rjb@cl.cam.ac.uk)
Efficiency in a Fully-Expansive Theorem Prover
PhD Thesis. University of Cambridge Computer Laboratory Technical Report 337, May 1994.
DVI / Abstract / Web Page.

Jonathan Bowen (Jonathan.Bowen@comlab.ox.ac.uk) and
Mike Gordon (mjcg@cl.cam.ac.uk)
Z and HOL
Invited contribution to the 8th Z User Meeting (ZUM'94), St John's College, University of Cambridge, UK, June 1994. Springer-Verlag, Workshops in Computing series. Organized by the Z User Group in association with BCS FACS.
PostScript.

Michael J. C. Gordon (mjcg@cl.cam.ac.uk)
Mechanizing Programming Logics in Higher Order Logic
In G. Birtwistle and P. A. Subrahmanyam (editors),
Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, 1989.
DVI.

Mike Gordon (mjcg@cl.cam.ac.uk) and Andrew Pitts (ap@cl.cam.ac.uk)
The HOL Logic and System
In J. Bowen (editor), Towards Verified Systems, Elsevier, Real-Time Safety Critical Systems series, volume 2, 1994.
Description of the syntax and semantics of the HOL logic and a brief overview of the theorem proving infrastructure. Condensed from Introduction to HOL by Gordon and Melham.
DVI / PostScript.

M. J. C. Gordon (mjcg@cl.cam.ac.uk)
State Transition Assertions: A Case Study
In J. Bowen (editor), Towards Verified Systems, Elsevier, Real-Time Safety Critical Systems series, volume 2, 1994.
DVI / PostScript.

Mike Gordon (mjcg@cl.cam.ac.uk)
A Mechanized Hoare Logic of State Transitions
In A. W. Roscoe (editor), A Classical Mind: Essays in Honour of C. A. R. Hoare, Prentice-Hall International Series in Computer Science, 1994. Companion paper to State Transition Assertions: A Case Study.
DVI / PostScript.

Mike Gordon (mjcg@cl.cam.ac.uk)
A Formalization of a Simplified Subset of the Alpha Shared Memory Model
Draft paper.
DVI / PostScript.

Mike Gordon (mjcg@cl.cam.ac.uk)
Memory Access Semantics for a Multiprocessor Instruction Set
Draft paper.
DVI / PostScript.

Mike Gordon (mjcg@cl.cam.ac.uk)
The Semantic Challenge of Verilog HDL
Revised version of an invited contribution to the Tenth Annual IEEE Symposium on Logic in Computer Science, San Diego, California, June 1995.
PostScript.

Jim Grundy (Jim.Grundy@abo.fi)
A Method of Program Refinement
PhD Thesis. University of Cambridge Computer Laboratory Technical Report 318, November 1993.
PostScript / Abstract / Directory.

John Harrison (jrh@cl.cam.ac.uk) and Laurent Théry (Laurent.Thery@inria.fr)
Extending the HOL theorem prover with a Computer Algebra System to Reason about the Reals
In J. J. Joyce and C.-J. H. Seger (editors), Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications (HUG'93), Vancouver, B.C., Canada, August 1993. Lecture Notes in Computer Science volume 780, Springer-Verlag, 1994.
PostScript.

John Harrison (jrh@cl.cam.ac.uk)
Metatheory and Reflection in Theorem Proving: A Survey and Critique
Technical Report CRC-053, SRI International Cambridge Computer Science Research Centre, Cambridge, UK. February 1995
DVI / PostScript.

Bart Jacobs and Tom Melham (tfm@dcs.gla.ac.uk)
Translating Dependent Type Theory into Higher Order Logic.
In M. Bezem and J. F. Groote (editors), Typed Lambda Calculi and Applications: Proceedings of the International Conference, Utrecht, The Netherlands, March 1993, pages 209-229. Lecture Notes in Computer Science volume 664, Springer-Verlag.
PostScript.

Thomas F. Melham (tfm@dcs.gla.ac.uk)
Using Recursive Types to Reason about Hardware in Higher Order Logic
In G. J. Milne (editor), The Fusion of Hardware Design and Verification: Proceedings of the IFIP WG 10.2 Working Conference, Glasgow, July 1988, pages 27-50. North-Holland.
DVI / PostScript.

Thomas F. Melham (tfm@dcs.gla.ac.uk)
The HOL Logic Extended with Quantification over Type Variables
In L. J. M. Claesen and M. J. C. Gordon (editors), Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2 Workshop, Leuven, Belgium, September 1992. IFIP Transactions volume A-20, North-Holland/Elsevier. (A later version is in Formal Methods in System Design, 3(1/2):7-24, August 1993.)
PostScript.

T. F. Melham (tfm@dcs.gla.ac.uk)
A Mechanized Theory of the pi-calculus in HOL
Nordic Journal of Computing, 1(1):50-76, Spring 1994.
PostScript.

Donald Syme (drs1004@cl.cam.ac.uk)
Machine Assisted Reasoning About Standard ML Using HOL
Bachelor's Thesis, Australian National University, Canberra, ACT, Australia, November 1992.
PostScript.

Donald Syme (drs1004@cl.cam.ac.uk)
Reasoning with the Formal Definition of Standard ML in HOL
In J. J. Joyce and C.-J. H. Seger (editors), Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications (HUG'93), Vancouver, B.C., Canada, August 1993. Lecture Notes in Computer Science volume 780, Springer-Verlag, 1994.
PostScript.

Donald Syme (drs1004@cl.cam.ac.uk)
A New Interface for HOL - Ideas, Issues and Implementation
In Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah, USA, September 1995. To be published by Springer-Verlag.
PostScript.

John Peter Van Tassel (jvt@ti.com)
Femto-VHDL: The Semantics of a Subset of VHDL and its Embedding in the HOL Proof Assistant
PhD Thesis. University of Cambridge Computer Laboratory Technical Report 317, November 1993.
Abstract / Directory.


Back to index for the Cambridge FTP Area for HOL
In case of difficulty send electronic mail to hol-support@cl.cam.ac.uk.

Photographs from HOL and QED Workshops


HOL Workshops

Details of HOL Workshops can be found here.

QED Workshops


Back to index for the Cambridge FTP Area for HOL
In case of difficulty send electronic mail to hol-support@cl.cam.ac.uk.

Archive of the QED Project


Back to index for the Cambridge FTP Area for HOL
In case of difficulty send electronic mail to hol-support@cl.cam.ac.uk.



Lab | ARG | Description | HOL | Isabelle | Members | Haiku

Page last updated on Tue Oct 10 17:56:25 BST 2000
by Daryl (djs1002@cl.cam.ac.uk)