Dale Miller is an American computer scientist and author. He is a Director of Research at Inria Saclay and one of the designers of the λProlog programming language and the Abella theorem prover. Miller is most known for his research on topics in computational logic, including proof theory, automated reasoning, and formalized meta-theory. He has co-authored the book Programming with Higher-order Logic. Miller is a Fellow of the Association for Computing Machinery (ACM), has been a two-term Editor-in-Chief of the ACM Transactions on Computational Logic from 2009 to 2015 and holds an editorial appointment on the Journal of Automated Reasoning. Early life and education In the 1970s, Miller published an Advanced Problem (Problem H-237) in the Fibonacci Quarterly, where his name was misread as “D. A. Millin”. The subject of that problem is now known as the Millin Series. He graduated with a B.S. in mathematics from Lebanon Valley College in 1978 and earned a Ph.D. in mathematics in 1983 under the supervision of Peter B. Andrews. Career Following his Ph.D., Miller started his academic career as an assistant professor at the University of Pennsylvania in 1983 and was promoted to associate professor in 1989. From 1997 to 2001, he was the Department Head of the Department of Computer Science and Engineering at the Pennsylvania State University. He was a professor at the Ecole Polytechnique from 2002 to 2006. Having moved to France in 2002, he is currently a Director of Research at Inria Saclay and was the scientific leader of the Parsifal team at Inria Saclay for 12 years. Research Miller's research spans the area of computational logic and focuses on proof theory, automated reasoning, unification theory, operational semantics, and logic programming. He is best known as one of the designers of the λProlog programming language and the Abella theorem prover. In addition to other honors, he has received two LICS Test-of-Time awards and an ERC Advanced Grant. Logic programming and formalized meta-theory Miller and Gopalan Nadathur co-developed the logic programming language λProlog, which is based on higher-order intuitionistic logic and was the first programming language to directly support λ-tree syntax (also known as higher-order abstract syntax). Since the language's introduction in 1985, various implementations have been made, including ELPI and Teyjus. With Alwen Tiu, Miller extended the proof theory for fixed points and first-order quantification to incorporate λ-tree syntax. Their analysis showed that negation-as-failure forces a distinction between