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 
<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 
<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

------------------------------------------------------------------------------
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