Thanks you for writing this article on the contributions of Mike Gordon.
I started using HOL4 days before he unfortunately died so I missed the
opportunity to know him personally. Your article made me more aware of
the lasting and positive impact he made to the field of formal
verification. People
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
