news@heitis1.uucp (News Administrator) (10/09/90)
We recently received information regarding HOL. It tells us what machine to get it from, but not much about it. Actually, much may have been told to someone else, but finally someone said "Look at this wierd address, and what is FTP??? Let's ask Brian" ;-). What I am interested in, is a "short" synopsis of what it does, and possibly a little about how it is programmed. Basically, I am fishing for information. Any help I could get would be greatly appreciated. brian
jack@cs.glasgow.ac.uk (Jack Campin) (10/11/90)
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