Dale Miller (academic)

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.

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 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. 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 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
*2014 – LICS Test-of-Time Award, LICS
*2021 – Fellow, Association for Computing Machinery
*2022 – Fellow, Asia-Pacific Artificial Intelligence Association (AAIA)
*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.

Bibliography

Books

*Miller, D. & Nadathur, G. (2012) ''Programming with higher-order logic'', ISBN 9780521879408, Cambridge University Press.

Selected articles

*Nadathur, G., & Miller, D. (1988). An overview of λProlog. Fifth International Logic Programming Conference, 810–827.
*Miller, D. (1989). A logical analysis of modules in logic programming. The Journal of Logic Programming, 6(1-2), 79–108.
*Miller, D., Nadathur, G., Pfenning, F., & Scedrov, A. (1991). Uniform proofs as a foundation for logic programming. Annals of Pure and Applied logic, 51(1-2), 125–157.
*Miller, D. (1991). A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4), 497–536.
*Miller, D. (1992). Unification under a mixed prefix. Journal of symbolic computation, 14(4), 321–358.
*Hodas, J. S., & Miller, D. (1994). Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2), 327–365.
*Miller, D., & Tiu, A. (2005). A proof theory for generic judgments. ACM Transactions on Computational Logic, 6(4), 749–783.
*Liang, C. & Miller, D. (2009). Focusing and Polarization in Linear, Intuitionistic, and Classical Logics. Theoretical Computer Science, 410(46), 4747–4768.
*Gacek, A., Miller, D., & Nadathur, G. (2011). Nominal abstraction. Information and Computation 209(1), 48–73.
*Chihani, Z., Miller, D., & Renaud, F. (2017). A semantic framework for proof evidence. Journal of Automated Reasoning. 59(3) 287–330.
*Miller, D. (2022). A survey of the proof-theoretic foundations of logic programming. Theory and Practice of Logic Programming, 22(6), 859–904.

References

{{DEFAULTSORT:Miller, Dale
American computer scientists
American scientists
American writers
Carnegie Mellon University alumni
Living people
Lebanon Valley College alumni
University of Pennsylvania faculty
Academic staff of École Polytechnique
Year of birth missing (living people)