[TYPES] Foundations of Mathematics: Type Theory after Church's Simple Theory of Types (1940)

[Ken Kubota]

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