Not quite a correction, but an important addendum to the last part ("Legacy")
is type abstraction, which Mike Gordon suggested for HOL (but didn't
implement), shaping future research. He already foresaw a binding of variables
connecting both term and type (subscript) level. (Gordon positively refers to
Tom Melham's extension of HOL [Gordon, 2000, p. 175, fn. 7]. R0 incorporates
type abstraction as a standard feature.)
Mike Gordon suggesting type abstraction for HOL: “The syntax and semantics of
type variables are currently being studied by several logicians. A closely
related area is the theory of ‘second order’ λ-terms like λα. λx:α. x, perhaps
such terms should be included in the HOL logic.” [Gordon, 2001, p. 22]
http://www.owlofminerva.net/files/fom.pdf
<http://www.owlofminerva.net/files/fom.pdf>, p. 7
Besides this, the article is excellent.
I was astonished that it even mentions the awareness of social class
distinctions (white vs. brown coats), as in
http://www.cl.cam.ac.uk/archive/mjcg/plans/NorthThamesGasBoard.html#white-versus-brown-coats
<http://www.cl.cam.ac.uk/archive/mjcg/plans/NorthThamesGasBoard.html#white-versus-brown-coats>
https://arxiv.org/pdf/1806.04002.pdf
<https://arxiv.org/pdf/1806.04002.pdf>, p. 2
Ken Kubota
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
> Am 07.07.2018 um 16:16 schrieb Lawrence Paulson <l...@cam.ac.uk>:
>
> Colleagues may be interested in my biographical article on Mike Gordon, whose
> promotion of higher-order logic has had such a profound impact on our field.
>
> https://arxiv.org/abs/1806.04002
>
> Corrections welcome.
>
> Larry Paulson
>
>
>
>
> ------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
