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

Reply via email to