Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!strath-cs!cs.glasgow.ac.uk!jack
From: jack@cs.glasgow.ac.uk (Jack Campin)
Newsgroups: comp.lang.misc
Subject: Re: What is HOL?
Message-ID: <6540@vanuata.cs.glasgow.ac.uk>
Date: 11 Oct 90 16:30:14 GMT
References: <1990Oct08.222547.5167@heitis1.uucp>
Reply-To: jack@cs.glasgow.ac.uk (Jack Campin)
Organization: COMANDOS Project, Glesga Yoonie, Unthank
Lines: 18
Summary:
Expires:
Sender:
Followup-To:
Keywords:

news@heitis1.uucp (News Administrator) wrote:
> We recently received information regarding HOL.  It tells us what machine
> to get it from, but not much about it. [...]  What I am interested in, is
> a "short" synopsis of what it does, and possibly a little about how it is
> programmed.

It stands for Higher-Order Logic, and is a theorem prover for digital
hardware verification using a fragment of Church's type theory.  It was
developed by Mike Gordon at Cambridge University.  It uses some of the
same lower-level stuff as Larry Paulson's ISABELLE.  It's written in ML.
That's all I know about it.  Try an enquiry to comp.specification for more
details.

-- 
--  Jack Campin   Computing Science Department, Glasgow University, 17 Lilybank
Gardens, Glasgow G12 8QQ, Scotland   041 339 8855 x6044 work  041 556 1878 home
JANET: jack@cs.glasgow.ac.uk    BANG!net: via mcsun and ukc   FAX: 041 330 4913
INTERNET: via nsfnet-relay.ac.uk   BITNET: via UKACRL   UUCP: jack@glasgow.uucp