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.


        author={Rob Arthan and Roger Bishop Jones},
        title="{Z in HOL in {\sf ProofPower}}",
        journal="BCS FACS FACTS",
        note= {\url{}},

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.


  author    = {Peter V. Homeier},
  title     = {The {HOL-Omega} Logic},
  booktitle = {TPHOLs},
  year      = {2009},
  pages     = {244-259},
  ee        = {},
  crossref  = {DBLP:conf/tphol/2009},
  bibsource = {DBLP,}

Best regards,


> On 15 Oct 2016, at 22:12, Ken Kubota <> 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
> 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’.",
>  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.",
>, 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
> ------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most 
> engaging tech sites,!
> _______________________________________________
> hol-info mailing list

Check out the vibrant tech community on one of the world's most 
engaging tech sites,!
hol-info mailing list

Reply via email to