| 2026 | FSCD | Treating Congruences as Equalities Within Proofs. | Dale Miller |
| 2026 | IJCAR | Automating Proof Search when Equality is a Logical Connective. | Kaustuv Chaudhuri, Arunava Gantait, Dale Miller |
| 2025 | FSCD | Linear Logic Using Negative Connectives. | Dale Miller |
| 2025 | TABLEAUX | Designing a Safe Forward Chaining Tactic Using Productive Proofs. | Kaustuv Chaudhuri, Arunava Gantait, Dale Miller |
| 2023 | CSL | A Positive Perspective on Term Representation (Invited Talk). | Dale Miller, Jui-Hsuan Wu |
| 2023 | LICS | A system of inference based on proof search: an extended abstract. | Dale Miller |
| 2020 | ICDCIT | A Distributed and Trusted Web of Formal Proofs. | Dale Miller |
| 2020 | SLE | Extrinsically typed operational semantics for functional languages. | Matteo Cimini, Dale Miller, Jeremy G. Siek |
| 2019 | CPP | A proof-theoretic approach to certifying skolemization. | Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller |
| 2019 | PPDP | Property-Based Testing via Proof Reconstruction. | Roberto Blanco, Dale Miller, Alberto Momigliano |
| 2019 | PPDP | Functional programming with λ-tree syntax. | Ulysse Grard, Dale Miller, Gabriel Scherer |
| 2017 | CADE | Translating Between Implicit and Explicit Versions of Proof. | Roberto Blanco, Zakaria Chihani, Dale Miller |
| 2017 | CSL | Separating Functional Computation from Relations. | Ulysse Grard, Dale Miller |
| 2016 | AiML | A focused framework for emulating modal proof systems. | Sonia Marin, Dale Miller, Marco Volpe |
| 2015 | CPP | A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. | Kaustuv Chaudhuri, Matteo Cimini, Dale Miller |
| 2015 | LOPSTR | Proof Checking and Logic Programming. | Dale Miller |
| 2015 | LPAR | Defining the meaning of TPTP formatted proofs. | Roberto Blanco, Tomer Libal, Dale Miller |
| 2015 | LPAR | On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control. | Chuck C. Liang, Dale Miller |
| 2015 | LPAR | Focused Labeled Proof Systems for Modal Logic. | Dale Miller, Marco Volpe |
| 2015 | PPDP | Proof checking and logic programming. | Dale Miller |
| 2013 | CADE | Foundational Proof Certificates in First-Order Logic. | Zakaria Chihani, Dale Miller, Fabien Renaud |
| 2013 | CADE | Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract). | Zakaria Chihani, Dale Miller, Fabien Renaud |
| 2013 | CPP | Extracting Proofs from Tabled Proof Search. | Dale Miller, Alwen Tiu |
| 2013 | LICS | Unifying Classical and Intuitionistic Logics for Computational Control. | Chuck C. Liang, Dale Miller |
| 2012 | CSL | A Systematic Approach to Canonicity in the Classical Sequent Calculus. | Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller |
| 2011 | CPP | A Proposal for Broad Spectrum Proof Certificates. | Dale Miller |
| 2010 | APLAS | Reasoning about Computations Using Two-Levels of Logic. | Dale Miller |
| 2010 | CADE | Focused Inductive Theorem Proving. | David Baelde, Dale Miller, Zachary Snow |
| 2009 | LICS | A Unified Sequent Calculus for Focused Proofs. | Chuck C. Liang, Dale Miller |
| 2009 | PPDP | Algorithmic specifications in linear logic with subexponentials. | Vivek Nigam, Dale Miller |
| 2008 | CADE | Focusing in Linear Meta-logic. | Vivek Nigam, Dale Miller |
| 2008 | LICS | A Neutral Approach to Proof and Refutation in MALL. | Olivier Delande, Dale Miller |
| 2008 | LICS | Combining Generic Judgments with Recursive Definitions. | Andrew Gacek, Dale Miller, Gopalan Nadathur |
| 2007 | CADE | The Bedwyr System for Model Checking over Syntactic Expressions. | David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu |
| 2007 | CSL | Focusing and Polarization in Intuitionistic Logic. | Chuck C. Liang, Dale Miller |
| 2007 | CSL | Incorporating Tables into Proofs. | Dale Miller, Vivek Nigam |
| 2007 | CSL | From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic. | Dale Miller, Alexis Saurin |
| 2007 | LPAR | Least and Greatest Fixed Points in Linear Logic. | David Baelde, Dale Miller |
| 2006 | CADE | Representing and Reasoning with Operational Semantics. | Dale Miller |
| 2006 | GPCE | Roadmap for enhanced languages and methods to aid verification. | Gary T. Leavens, Jean-Raymond Abrial, Don S. Batory, Michael J. Butler, Alessandro Coglio, Kathi Fisler, Eric C. R. Hehner, Cliff B. Jones, Dale Miller, Simon L. Peyton Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump |
| 2006 | PPDP | Collection analysis for Horn clause programs. | Dale Miller |
| 2005 | LPAR | On the Specification of Sequent Systems. | Elaine Pimentel, Dale Miller |
| 2004 | CSL | Bindings, Mobility of Bindings, and the "generic judgments"-Quantifier: An Abstract. | Dale Miller |
| 2003 | LICS | A Proof Theory for Generic Judgments: An extended abstract. | Dale Miller, Alwen Fernanto Tiu |
| 2002 | TABLEAUX | Using Linear Logic to Reason about Sequent Systems. | Dale Miller, Elaine Pimentel |
| 1997 | LICS | A Logic for Reasoning with Higher-Order Abstract Syntax. | Raymond McDowell, Dale Miller |
| 1994 | LICS | A Multiple-Conclusion Meta-Logic | Dale Miller |
| 1993 | VR | The Simnet Virtual World Architecture. | James M. Calvin, Alan Dickens, Bob Gaines, Paul Metzger, Dale Miller, Dan Owen |
| 1993 | VR | Image Generation Design for Ground-based Network Training Environments. | Brian Soderberg, Dale Miller |
| 1992 | CSCW | Flexible Diff-ing in a Collaborative Writing System. | Christine Neuwirth, Ravinder Chandhok, David Kaufer, Paul Erion, James H. Morris, Dale Miller |
| 1991 | ICLP | Unification of Simply Typed Lamda-Terms as Logic Programming. | Dale Miller |
| 1991 | ICLP | Logics for Logic Programming: A Tutorial. | Dale Miller |
| 1991 | LICS | Logic Programming in a Fragment of Intuitionistic Linear Logic | Joshua S. Hodas, Dale Miller |
| 1991 | LPAR | Abstract Syntax and Logic Programming. | Dale Miller |
| 1990 | CADE | Tutorial on Lambda-Prolog. | Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning |
| 1990 | CADE | Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language. | Amy P. Felty, Dale Miller |
| 1990 | ICLP | Representing Objects in a Logic Programming Langueage with Scoping Constructs. | Joshua S. Hodas, Dale Miller |
| 1990 | ICLP | Higher-Order Logic Programming. | Dale Miller |
| 1990 | ICLP | Extending Definite Clause Grammars with Scoping Constructs. | Remo Pareschi, Dale Miller |
| 1989 | ICLP | Lexical Scoping as Universal Quantification. | Dale Miller |
| 1989 | MPC | Deriving Mixed Evaluation from Standard Evaluation for a Simple Functional Language. | John Hannan, Dale Miller |
| 1988 | CADE | Lambda-Prolog: An Extended Logic Programming Language. | Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov |
| 1988 | CADE | Specifying Theorem Provers in a Higher-Order Logic Programming Language. | Amy P. Felty, Dale Miller |
| 1988 | ICLP | Uses of Higher-Order Unification for Implementing Program Transformers. | John Hannan, Dale Miller |
| 1988 | ICLP | An Overview of Lambda-PROLOG. | Gopalan Nadathur, Dale Miller |
| 1987 | LICS | Hereditary Harrop Formulas and Uniform Proof Systems | Dale Miller, Gopalan Nadathur, Andre Scedrov |
| 1986 | AAAI | An Integration of Resolution and Natural Deduction Theorem Proving. | Dale Miller, Amy P. Felty |
| 1986 | ACL | Some Uses of Higher-Order Logic in Computational Linguistics. | Dale Miller, Gopalan Nadathur |
| 1986 | ICLP | Higher-Order Logic Programming. | Dale Miller, Gopalan Nadathur |
| 1984 | CADE | Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. | Dale Miller |