[ 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
