Personal profile
Personal profile
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.
Research interests
- Proof Theory
- Linear Logic
- Logic Programming
- Theorem Proving
- Computational Logic
Fingerprint
- 1 Similar Profiles
Collaborations and top research areas from the last five years
-
Designing a Safe Forward Chaining Tactic Using Productive Proofs
Chaudhuri, K., Gantait, A. & Miller, D., 1 Jan 2026, Automated Reasoning with Analytic Tableaux and Related Methods - 34th International Conference, TABLEAUX 2025, Proceedings. Pozzato, G. L. & Uustalu, T. (eds.). Springer Science and Business Media Deutschland GmbH, p. 299-317 19 p. (Lecture Notes in Computer Science; vol. 15980 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
Open Access -
Linear Logic Using Negative Connectives
Miller, D., 7 Jul 2025, 10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025. Fernandez, M. (ed.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 29. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 337).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
-
About Trust and Proof: An Experimental Framework for Heterogeneous Verification
Al Wardani, F., Chaudhuri, K. & Miller, D., 1 Jan 2024, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Science and Business Media Deutschland GmbH, p. 162-183 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. LNCS 14781).Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review
Open Access -
Focusing Gentzen’s LK Proof System
Liang, C. & Miller, D., 1 Jan 2024, Outstanding Contributions to Logic. Springer Science and Business Media B.V., p. 275-313 39 p. (Outstanding Contributions to Logic; vol. 29).Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review
Open Access -
Property-Based Testing by Elaborating Proof Outlines
Miller, D. & Momigliano, A., 1 Jan 2024, (Accepted/In press) In: Theory and Practice of Logic Programming. S1471068424000176.Research output: Contribution to journal › Article › peer-review
Open Access -
A Positive Perspective on Term Representation
Miller, D. & Wu, J. H., 1 Feb 2023, 31st EACSL Annual Conference on Computer Science Logic, CSL 2023. Klin, B. & Pimentel, E. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 3. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 252).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
-
A system of inference based on proof search: an extended abstract
Miller, D., 1 Jan 2023, 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023. Institute of Electrical and Electronics Engineers Inc., (Proceedings - Symposium on Logic in Computer Science; vol. 2023-June).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
Open Access -
Formal Reasoning Using Distributed Assertions
Al Wardani, F., Chaudhuri, K. & Miller, D., 1 Jan 2023, Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Proceedings. Sattler, U. & Suda, M. (eds.). Springer Science and Business Media Deutschland GmbH, p. 176-194 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14279 LNAI).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
Open Access -
A Survey of the Proof-Theoretic Foundations of Logic Programming
Miller, D., 1 Nov 2022, In: Theory and Practice of Logic Programming. 22, 6, p. 859-904 46 p.Research output: Contribution to journal › Article › peer-review
Open Access -
From axioms to synthetic inference rules via focusing
Marin, S., Miller, D., Pimentel, E. & Volpe, M., 1 May 2022, In: Annals of Pure and Applied Logic. 173, 5, 103091.Research output: Contribution to journal › Article › peer-review
Open Access