coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Ken Kubota <mail AT kenkubota.de>
To: coq-club AT inria.fr
Cc: "Prof. Thierry Coquand" <coquand AT chalmers.se>, "Prof. Gérard Huet" <Gerard.Huet AT inria.fr>, "Prof. Christine Paulin-Mohring" <Christine.Paulin AT lri.fr>
Subject: [Coq-Club] Foundations of Mathematics: Type Theory after Church's Simple Theory of Types (1940)
Date: Fri, 4 Nov 2016 19:40:37 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT kenkubota.de; spf=Pass smtp.mailfrom=mail AT kenkubota.de; spf=None smtp.helo=postmaster AT plasma5.jpberlin.de
Ironport-phdr: 9a23:l7ihnxVHB2ReutSUm8yJana1I5TV8LGtZVwlr6E/grcLSJyIuqrYZhCOt8tkgFKBZ4jH8fUM07OQ6PG6HzxRqs/Y7jgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLHovc2CKFwR2nKUWvBbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4/SXEGACI/z4XVngcuhtOGQnMqh/gDbnrtS6vled7kAqHN8rqRPhgXD2j649oRRnrlS0AKzd//GyB2Z84t75SvB/0/083+IXTeozAcaMmJq4=

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 Lawrence C. Paulson) as well
as
- Andrews' Q0 (including Tom Melham's extension of HOL drawing on the work of
Andrews)
and other systems (e.g., Coq) 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.
The quotes concerning Coq can be found on p. 7 (general description) and p. 8
(critique).

Due to limited space, unfortunately not all people contributing to existing
projects could be mentioned. 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

[Coq-Club] Foundations of Mathematics: Type Theory after Church's Simple Theory of Types (1940), Ken Kubota, 11/04/2016