Dale Allen Miller

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 interactive 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 1973, while a senior at the Annville-Cleona High School, 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 École 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 interactive theorem prover. In addition to other honors, he has received two LICS Test-of-Time awards and an ERC Advanced Grant.

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 generic and universal quantification. They introduced the ∇-quantifier to capture the generic quantifier. Their extended logical system could directly capture many model-checking and meta-theoretical aspects of the π-calculus.

Working with Nadathur, Tiu, Andrew Gacek, and Kaustuv Chaudhuri, Miller helped design the Abella interactive theorem prover. Since this prover directly supports λ-tree syntax, it is possible to use it to reason inductively and coinductively on syntactic objects containing binding. This prover has successfully been applied to the formalized meta-theory of the λ-calculus, the π-calculus, and to programming languages specified using operational semantics. Working with Chuck Liang, he has helped to develop the notion of focused sequent calculus proof. This particular style of proof system was used as the basis of his 2012 ERC advanced grant awarded, ProofCert, in which a wide range of proof certificate formats could be defined and immediately implemented.

Miller has also made use of linear logic within computer science. In particular, he has demonstrated applications of linear logic to natural language parsing, operational semantic specifications, model checking, and the specification of proof systems for classical, intuitionistic, and linear logics.

Miller has also written about the unification of λ-calculus expressions, focusing, in particular, on the treatment of such unification when it is done under both existential and universal quantifiers, and on the identification of the pattern unification fragment of higher-order unification, a fragment that strongly resembles first-order unification while treating binders with the usual rules for λ-conversion.

Awards and honors 1974 – Finalist in the 33rd Westinghouse Science Talent Search (now the Regeneron Science Talent Search) 2011 – LICS Test-of-Time Award, LICS 2023 – Co-recipient of the Dov Gabbay Prize for Logic and Foundations for 2023.

Personal life Miller lives in France. He is married to Catuscia Palamidessi and has two children.