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. Computational logic and proof theory Miller has conducted research on computational logic and proof theory, with a particular emphasis on applying proof theory concepts to computer science issues. Over the years, his work has concentrated on using the proof-search approach to interpret proof theory to computational logic. He has shown that proof theory can provide a fruitful foundation for logic programming in classical, intuitionistic, and linear logics. 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 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 2014 – LICS Test-of-Time Award, LICS 2021 – Fellow, Association for Computing Machinery 2022 – Fellow, Asia-Pacific Artificial Intelligence Association (AAIA) Personal life Miller lives in France. He is married to Catuscia Palamidessi and has two children. Bibliography Books Programming with higher-order logic (2012) ISBN 9780521879408 Selected articles Nadathur, G., & Miller, D. (1988). An overview of λProlog. Fifth International Logic Programming Conference, 810–827. Miller, D. (1989). A logical analysis