Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: hol2000@leopard.cs.byu.edu
In-Reply-To: <199503171855.AA087046529@jaguar.cs.byu.edu> (black@lal.cs.byu.edu)
Subject: Re: where's parallel HOL?
Message-Id: <95Mar18.173139met.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Sat, 18 Mar 1995 17:31:34 +0100


> HOL 2000 should be a parallel/distributed implementation.  Who's
> working on a parallel version of *ML, etc.?

I fully agree: I think there are interesting possibilities in
"groupware" for theorem proving, and a necessary component for that is
distribution (not just threads, ala CML). A distributed ML that exists
is FACILE, which builds in ideas from CHOCS and the pi-calculus. FACILE
is built on top of SML/NJ 0.93, and was released in July of last
year. Here's a paragraph from the release announcement:

    Facile enriches Standard ML with primitives for distribution,
    concurrency and communication over typed channels.  The additional
    data types provided in the language include node identifiers,
    process scripts and communication channels.  All of these are
    first-class values that can be manipulated in an applicative style
    and, in particular, be communicated.  New nodes and channels can be
    created dynamically and processes executing a given script can be
    spawned dynamically on a given node.

The following report

    Thomsen, B., Leth, L., Prasad, S., Kuo, T.-S., Kramer, A., Knabe, F.,
    Giacalone, A.:
    "Facile Antigua Release -- Programming Guide",
    Technical report ECRC-93-20, 1993.

and other ECRC technical reports can be obtained via ftp from
ftp.ecrc.de (141.1.1.1).  Log in as "anonymous". The report ECRC-93-20
is stored under the directory "pub/ECRC_tech_reports/reports" as
ECRC-93.20.ps.Z.  There is a README file (in directory
"pub/ECRC_tech_reports") containing some further information.


Konrad.