Dale Miller

Winner of the Dov Gabbay Prize 2023

INRIA Saclay & Laboratoire d’Informatique, LIX, Ecole Polytechnique (France)

Dale Miller received his Ph.D. in Mathematics in 1983 from Carnegie Mellon University. In that year he joined the Pennsylvania State University where he was promoted to full professor in the Department of Computer Science and Engineering in 1997. In 2002 he got a professorship at the renowned Ecole Polytechnique in France. Since 2018 he has also been Director of Research (classe exceptionnelle) at Inria Saclay. In 2011 and 2014 he received LICS Test-of-Time awards. In 2021 he was named a Fellow of the ACM for his contributions to proof theory and computational logic, and in 2022 also fellow of the Asia-Pacific Artificial Intelligence Association (AAIA). Numerous visiting positions have allowed to increase the impact of his groundbreaking research.

The centre of his investigations has been the interplay between proof theory and computational logic. His work illustrates the beneficial cross-fertilization between basic research on the foundations of proof and the actual construction of computational systems (e.g., 1987, 1992 and 1991). His research has generated new insights into the nature and application of proofs in first-order and higher-order versions of classical, intuitionistic, and linear logics (e.g., 2009).

Miller also developed computational logic software implementations that build upon his results, including a reference implementation for the logic programming language λProlog (2012), the Abella theorem prover (2014), and the Bedwyr model checker (2018). He also presented an implementation of the Foundational Proof Certificate framework for defining and checking proof evidence in classical and intuitionistic logics (2016).

Image source: Inria/Dale Miller