Email Gateway (Aug 22 2022 at 14:16): Email Gateway (Aug 22 2022 at 14:16):From: Ken Kubota <mail@kenkubota.de>
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),
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
Last updated: Apr 20 2024 at 01:05 UTC