Dear Rob,
dear Peter,
Thank you very much for your hints.
I have added ProofPower and HOL-Omega (and also Norbert Völker's HOL2P to which
it refers) to the overview at
http://dx.doi.org/10.4444/100.111
Furthermore, a reference to a comparison of logics by Freek Wiedijk was made,
which I found helpful.
Best regards,
Ken
____________________
Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100
> Am 17.10.2016 um 12:23 schrieb Rob Arthan <r...@lemma-one.com>:
>
> Ken,
>
> Thanks for sharing this interesting work.
>
> Two implemented systems that are alive and kicking and that
> you might like to be aware of are:
>
> ProofPower: a member of the HOL family contemporary with HOL4
> and designed with industrial applications in view. Its design aims include:
> support for readable well-documented specifications as well as proof;
> support for other formal languages via semantic embedding
> (eventually picked up as a hot topic in all the other descendants of
> Mike Gordon’s HOL). The main architect was Roger Bishop Jones.
>
> References:
>
> @article{proofpower,
> author={Rob Arthan and Roger Bishop Jones},
> title="{Z in HOL in {\sf ProofPower}}",
> journal="BCS FACS FACTS",
> year="2005-1",
> note= {\url{http://www.lemma-one.com/ProofPower/index/}},
> }
>
> http://www.lemma-one.com/ProofPower/index/index.html
>
> HOL-Omega: Peter Homeier's implementation of
> quantification over types as an extension of HOL4. Inspired by
> Tom Melham’s ideas, it incorporates a much more powerful type system
> than Tom envisaged.
>
> References:
>
> @inproceedings{Homeier09,
> author = {Peter V. Homeier},
> title = {The {HOL-Omega} Logic},
> booktitle = {TPHOLs},
> year = {2009},
> pages = {244-259},
> ee = {http://dx.doi.org/10.1007/978-3-642-03359-9_18},
> crossref = {DBLP:conf/tphol/2009},
> bibsource = {DBLP, http://dblp.uni-trier.de}
> }
>
> http://www.trustworthytools.com/id17.html
>
> Best regards,
>
> Rob.
>
>> On 15 Oct 2016, at 22:12, Ken Kubota <m...@kenkubota.de> wrote:
>>
>> Dear Members of the Research Community,
>>
>> In an attempt to create a genealogy of the foundations of mathematics,
>> the main approaches based upon Church's Simple Theory of Types (1940),
>> - Gordon's HOL (including origins like Huet's and Paulson's LCF and the
>> descendants by Konrad Slind, John Harrison, and Larry Paulson) as well as
>> - Andrews' Q0 (including Tom Melham's extension of HOL drawing on the work
>> of Andrews)
>> are compared online at
>>
>> http://dx.doi.org/10.4444/100.111
>>
>> The purpose is to make design decisions transparent in order to
>> systematically characterize and compare logistic systems,
>> which either explicitly or implicitly try to express most or all of formal
>> logic and mathematics.
>>
>> Hints, comments, corrections and critique are welcome.
>>
>> Other systems (e.g., Coq) shall be considered at a later time.
>>
>> I wasn't sure concerning the history of Cambridge LCF, as its descriptions
>> slightly differ.
>> In one version, Paulson further develops the (finished) result by Huet, in
>> another they directly collaborate.
>> ("Huet’s Franz Lisp version of LCF was further developed at Cambridge by
>> Larry Paulson, and became known as ‘Cambridge LCF’.",
>> http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-description.pdf,
>> p. 4,
>> vs. "Paulson and Huet then established a collaboration and did a lot of
>> joint development of LCF by sending each other magnetic tapes in the post.",
>> http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf, p. 3.)
>> In the overview, it is summarized as "Cambridge LCF by Larry Paulson and
>> Gérard Huet (around 1985)",
>> as it seems important that both contributed, and Paulson's name later
>> appears in the context of Isabelle, and Huet's in the context of Coq.
>>
>> Due to limited space, unfortunately not all people contributing to existing
>> projects could be mentioned.
>> For example, I am well aware that Michael Norrish maintains and contributes
>> to HOL4.
>> I apologize for having to restrict the presentation, mentioning only the
>> initiators or project leaders.
>>
>> Kind regards,
>>
>> Ken Kubota
>>
>> ____________________
>>
>> Ken Kubota
>> doi: 10.4444/100
>> http://dx.doi.org/10.4444/100
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
