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

Reply via email to