Article View: comp.lang.misc
Article #1685Re: What is HOL?
From: Jack Campin
Date: Thu, 11 Oct 1990 16:30
Date: Thu, 11 Oct 1990 16:30
18 lines
1451 bytes
1451 bytes
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
Technical Details
Message-ID:
<6540@vanuata.cs.glasgow.ac.uk>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!strath-cs!cs.glasgow.ac.uk!jackReferences:
<1990Oct08.222547.5167@heitis1.uucp>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!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