Dale Miller received his Ph.D. in Mathematics in 1983 from Carnegie Mellon University. He has been a professor at the University of Pennsylvania and Ecole Polytechnique (France) and Department Head in Computer Science and Engineering at Pennsylvania State University. He has held visiting positions at the Australian National University and the universities of Aix-Marseille, Sienna, Genoa, Pisa, and Edinburgh. He is currently Director of Research (classe exceptionnelle) at Inria Saclay. He has been the Scientific Leader of the Parsifal team from 2004-2019.
Miller was a two-term editor-in-chief of the ACM Transactions on Computational Logic and is a member of the editorial board of the Journal of Automated Reasoning. He was the General Chair for LICS from 2018 to 2021. In 2014 he was a PC chair for CSL and LICS. He was awarded an ERC Advanced Grant in 2011 and the LICS Test-of-Time awards in 2011 and 2014 for papers written in 1991 and 1994. He is an ACM Fellow and a recipient of the Dov Gabbay Prize for Logic and Foundations in 2023.
Miller works on various topics in computational logic, including proof theory, automated reasoning, logic programming, unification theory, operational semantics, and proof certificates. He is one of the designers of the λProlog programming language and the Abella theorem prover.
Dale Miller, Ph.D. Carnegie Mellon University 1983. Proofs in Higher-order Logic. Advised by Peter Andrews.
Andrews, Ph.D. Princeton University 1964. A Transfinite Type Theory with Type Variables. Advised by Alonzo Church. Recipient of the 2003 Herbrand Award for Advances in Automated Reasoning.
Church, Ph.D. Princeton University 1927. Alternatives to Zermelo's Assumption. Advised by Oswald Veblen.
At this point, many people trained in either mathematics or computer science in the USA share this genealogy. The following list of ancestors was published by Dick Lipton on his blog.
Veblen, Ph.D. University of Chicago 1903, A System of Axioms for Geometry under Eliakim Moore.
Moore, 1885, Yale, under Hubert Newton. Here Moore is listed as having over 15,000 descendants-more than 1/10 of the entire tree-and Veblen has roughly half of them.
Newton only earned a BA. This is somewhat like being adopted. However, an advisor Michel Chasles is listed for the B.A., and the other descendants include the renowned mathematical physicist Josiah Gibbs.
Chasles, 1814, École Polytechnique under Siméon Poisson. Now we are in even more august company-Poisson's other doctoral students were Lejeune Dirichlet and Jospeh Liouville.
Poisson, 1800, also École Polytechnique, and another co-advisee: Joseph Lagrange and Pierre-Simon Laplace.
Going through Lagrange hits Leonhard Euler, while Laplace's advisor was Jean d'Alembert.