Automated Reasoning Group Old FTP Area for HOL
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:
- name of the subdirectory
- a one-line description of the contents
- names and addresses of the authors
- date of inclusion in contrib
Contributors may also include other information in the READ-ME file.
- 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.
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.
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)