For the latest release see the current FTP page.

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.

- Source code for Hol98
- Source code for HOL90
- Source code and manuals for HOL88
- Technical Reports
- Papers and Theses
- Papers from poster session at the 1994 HOL Workshop
- Photographs from HOL and QED Workshops
- Archive of the QED project
- Archive of the info-hol mailing list (no longer maintained)
- Archive of the hol2000 mailing list

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.

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.

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.

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.

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

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:

- name of the subdirectory
- a one-line description of the contents
- names and addresses of the authors
- date of inclusion in
`contrib`

**ind-defs**by John Harrison (95.05.08)- Mutually inductive definitions with arbitrary monotone hypotheses
**TkHolWorkbench**by Donald Syme (95.04.04)- Interface for HOL implemented using the Tk toolkit
**cpo**by Wishnu Prasetya (94.06.01)- Theory of CPOs and lattices
**DerLem**by Wishnu Prasetya (94.03.23)- 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.

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.

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.

- 1988 HOL Workshop (2.5 MBytes)
- 1989 HOL Workshop (4.3 MBytes)
- 1990 HOL Workshop (1.3 MBytes)
- 1992 HOL Workshop (1.3 MBytes)
- 1993 HOL Workshop (2.6 MBytes)
- 1994 HOL Workshop (1.0 MBytes)

- 1st QED Workshop (1994) (2.8 MBytes)

Back to index for the Cambridge FTP Area for HOL

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

Back to index for the Cambridge FTP Area for HOL

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

by Daryl (djs1002@cl.cam.ac.uk)