Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9411030911.AA19315@bolverk.cs.cornell.edu>
To: Konrad Slind <slind@informatik.tu-muenchen.de>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: bhogan@bedlam: HOL90 on a PC
In-Reply-To: Your message of "Thu, 03 Nov 1994 10:03:08 +0100." <94Nov3.100322met.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 03 Nov 1994 04:11:36 -0500
From: Chet Murthy <murthy@cs.cornell.edu>


>>>>> "KS" == Konrad Slind <slind@informatik.tu-muenchen.de> writes:

    KS> Yes! But it doesn't make sense to do ad-hoc ports: the right
    KS> thing to do is develop a portable HOL, and then port
    KS> that. (Note that a portable system should be more
    KS> self-contained and therefore less apt to use *fantastic* new
    KS> goodies (or even ML-Yacc).) Probably the most portable system
    KS> would be implemented purely in the SML Core language, (maybe
    KS> plus structures to give separate namespaces).

Such a HOL would be pretty unmaintainable, no?  I mean, it would be
pretty low-level code.  Perhaps a better strategy would be to get
somebody to write a general-purpose set of
code-reduction/transformation tools for ML that could be used to
convert SML+Functors into Core ML and then print it out?

    KS> Of course, nobody wants to have to translate:

A mechanical translator from SML to caml-light for everything but the
functor-language is more than feasible -- its almost trivial.  I was
pointing out, though, that even doing it by hand, when one is dead
tired (I did 20K lines in 3 days straight, including the time it took
me to do some simple debugging, over Christmas 1992), its trivial.

    KS> HOL2000/QED thought: could agreement on a concrete (or
    KS> abstract) syntax for the term language happen for the large
    KS> number of HOL-like theorem provers?

There is already agreement over at least one common abstract syntax --
Edinburgh LF.  I suspect that *all* term-languages for provers could
be easily translated into LF -- certainly Constructions and Nuprl can,
and I'd bet that HOL could, too.

--chet--