[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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

Reply via email to