| Dale Miller | Ph.D. Carnegie Mellon University 1983 Proofs in Higher-Order Logic |
| Peter Andrews | Ph.D. Princeton University 1964 A Transfinite Type Theory with Type Variables Recipient of the 2003 Herbrand Award for Advances in Automated Reasoning |
| Alonzo Church | Ph.D. Princeton University 1927 Alternatives to Zermelo's Assumption |
| Oswald Veblen | Ph.D. University of Chicago 1903 A System of Axioms for Geometry |
At this point, a great many people trained in mathematics and computer science in the USA share this genealogy. The following list of ancestors was written by Dick Lipton on his blog.