A Look at TPS. - Dale A. Miller; Eve Longini Cohen; Peter B. Andrews (CADE, 1982)

Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. - Dale Miller 001 (CADE, 1984)

An Integration of Resolution and Natural Deduction Theorem Proving. - Dale Miller 001; Amy P. Felty (AAAI, 1986)

Some Uses of Higher-Order Logic in Computational Linguistics. - Dale Miller 001; Gopalan Nadathur (ACL, 1986)

Research in Natural Language Processing. - Aravind K. Joshi; Timothy W. Finin; Dale Miller 001; Lokendra Shastri; Bonnie L. Webber (HLT, 1986)

Higher-Order Logic Programming. - Dale Miller 001; Gopalan Nadathur (ICLP, 1986)

A Theory of Modules for Logic Programming. - Dale Miller 001 (SLP, 1986)

Hereditary Harrop Formulas and Uniform Proof Systems - Dale Miller 001; Gopalan Nadathur; Andre Scedrov (LICS, 1987)

A Logic Programming Approach to Manipulating Formulas and Programs. - Dale Miller 001; Gopalan Nadathur (SLP, 1987)

A compact representation of proofs. - Dale A. Miller (Stud Logica, 1987)

Lambda-Prolog: An Extended Logic Programming Language. - Amy P. Felty; Elsa L. Gunter; John Hannan; Dale Miller 001; Gopalan Nadathur; Andre Scedrov (CADE, 1988)

Specifying Theorem Provers in a Higher-Order Logic Programming Language. - Amy P. Felty; Dale Miller 001 (CADE, 1988)

Uses of Higher-Order Unification for Implementing Program Transformers. - John Hannan; Dale Miller 001 (ICLP/SLP, 1988)

An Overview of Lambda-PROLOG. - Gopalan Nadathur; Dale Miller 001 (ICLP/SLP, 1988)

A Meta-Logic for Functional Programming. - John Hannan; Dale Miller 001 (META, 1988)

Lexical Scoping as Universal Quantification. - Dale Miller 001 (ICLP, 1989)

Deriving Mixed Evaluation from Standard Evaluation for a Simple Functional Language. - John Hannan; Dale Miller 001 (MPC, 1989)

A Logical Analysis of Modules in Logic Programming. - Dale Miller 001 (J. Log. Program., 1989)

Tutorial on Lambda-Prolog. - Amy P. Felty; Elsa L. Gunter; Dale Miller 001; Frank Pfenning (CADE, 1990)

Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language. - Amy P. Felty; Dale Miller 001 (CADE, 1990)

Representing Objects in a Logic Programming Langueage with Scoping Constructs. - Joshua S. Hodas; Dale Miller 001 (ICLP, 1990)

Higher-Order Logic Programming. - Dale Miller 001 (ICLP, 1990)

Extending Definite Clause Grammars with Scoping Constructs. - Remo Pareschi; Dale Miller 001 (ICLP, 1990)

From Operational Semantics to Abstract Machines: Preliminary Results. - John Hannan; Dale Miller 001 (LISP and Functional Programming, 1990)

Higher-Order Horn Clauses - Gopalan Nadathur; Dale Miller 001 (J. ACM, 1990)

Unification of Simply Typed Lamda-Terms as Logic Programming. - Dale Miller 001 (ICLP, 1991)

Logics for Logic Programming: A Tutorial. - Dale Miller 001 (ICLP, 1991)

Abstract Syntax and Logic Programming. - Dale Miller 001 (RCLP, 1991)

Uniform Proofs as a Foundation for Logic Programming. - Dale Miller 001; Gopalan Nadathur; Frank Pfenning; Andre Scedrov (Ann. Pure Appl. Log., 1991)

A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. - Dale Miller 001 (J. Log. Comput., 1991)

Flexible Diff-ing in a Collaborative Writing System. - Christine Neuwirth; Ravinder Chandhok; David Kaufer; Paul Erion; James H. Morris; Dale Miller 001 (CSCW, 1992)

The pi-Calculus as a Theory in Linear Logic: Preliminary Results. - Dale Miller 001 (ELP, 1992)

Unification Under a Mixed Prefix. - Dale Miller 001 (J. Symb. Comput., 1992)

From Operational Semantics for Abstract Machines. - John Hannan; Dale Miller 001 (Math. Struct. Comput. Sci., 1992)

A Proposal for Modules in Lambda-Prolog. - Dale Miller 001 (ELP, 1993)

Specifications Using Multiple-Conclusion Logic Programs. - Dale Miller 001 (ALP, 1994)

A Multiple-Conclusion Meta-Logic - Dale Miller 001 (LICS, 1994)

Logic Programming in a Fragment of Intuitionistic Linear Logic - Joshua S. Hodas; Dale Miller 001 (Inf. Comput., 1994)

Annotations are not "for free": The Need for Runtime Layer Support in Hypertext Engines. - Christine M. Neuwirth; Ravinder Chandhok; David Kaufer; James H. Morris; Paul Erion; Dale Miller 001 (Designing User Interfaces for Hypermedia, 1995)

Observations about Using Logic as a Specification Language. - Dale Miller 001 (GULP-PRODE, 1995)

Linear Logic as Logic Programming: An Abstract. - Dale Miller 001 (LACL, 1996)

Logical Foundations for Open System Design. - Dale Miller 001 (ACM Comput. Surv., 1996)

Forum: A Multiple-Conclusion Specification Logic. - Dale Miller 001 (Theor. Comput. Sci., 1996)

A Logic for Reasoning with Higher-Order Abstract Syntax. - Raymond McDowell; Dale Miller 001 (LICS, 1997)

Foundational Aspects of Syntax. - Dale Miller 001; Catuscia Palamidessi (ACM Comput. Surv., 1999)

Abstract Syntax for Variable Binders: An Overview. - Dale Miller 001 (Computational Logic, 2000)

Cut-elimination for a logic with definitions and induction. - Raymond McDowell; Dale Miller 001 (Theor. Comput. Sci., 2000)

Encoding Generic Judgments: Preliminary results. - Dale Miller 001 (MERLIN, 2001)

Higher-Order Quantification and Proof Search. - Dale Miller 001 (AMAST, 2002)

Encoding Generic Judgments. - Dale Miller 001; Alwen Fernanto Tiu (FSTTCS, 2002)

Using Linear Logic to Reason about Sequent Systems. - Dale Miller 001; Elaine Pimentel (TABLEAUX, 2002)

Reasoning with higher-order abstract syntax in a logical framework. - Raymond McDowell; Dale Miller 001 (ACM Trans. Comput. Log., 2002)

A Proof Theory for Generic Judgments: An extended abstract. - Dale Miller 001; Alwen Fernanto Tiu (LICS, 2003)

Reasoning about Proof Search Specifications: An Abstract. - Dale Miller 001 (TPHOLs, 2003)

Encryption as an abstract data type. - Dale Miller 001 (WoLLIC, 2003)

Encoding transition systems in sequent calculus. - Raymond McDowell; Dale Miller 001; Catuscia Palamidessi (Theor. Comput. Sci., 2003)

Bindings, Mobility of Bindings, and the "generic judgments"-Quantifier: An Abstract. - Dale Miller 001 (CSL, 2004)

A Proof Search Specification of the pi-Calculus. - Alwen Fernanto Tiu; Dale Miller 001 (FGUC, 2004)

On the Specification of Sequent Systems. - Elaine Pimentel; Dale Miller 001 (LPAR, 2005)

A Proof Theoretic Approach to Operational Semantics. - Dale Miller 001 (APC 25, 2005)

A Game Semantics for Proof Search: Preliminary Results. - Dale Miller 001; Alexis Saurin (MFPS, 2005)

A Congruence Format for Name-passing Calculi. - Axelle Ziegler; Dale Miller 001; Catuscia Palamidessi (SOS@ICALP, 2005)

A proof theory for generic judgments. - Dale Miller 001; Alwen Tiu (ACM Trans. Comput. Log., 2005)

Representing and Reasoning with Operational Semantics. - Dale Miller 001 (IJCAR, 2006)

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 001; Simon L. Peyton Jones; Murali Sitaraman; Douglas R. Smith; et al. (GPCE, 2006)

Collection analysis for Horn clause programs. - Dale Miller 001 (PPDP, 2006)

The Bedwyr System for Model Checking over Syntactic Expressions. - David Baelde; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu (CADE, 2007)

Focusing and Polarization in Intuitionistic Logic. - Chuck C. Liang; Dale Miller 001 (CSL, 2007)

Incorporating Tables into Proofs. - Dale Miller 001; Vivek Nigam (CSL, 2007)

From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic. - Dale Miller 001; Alexis Saurin (CSL, 2007)

Least and Greatest Fixed Points in Linear Logic. - David Baelde; Dale Miller 001 (LPAR, 2007)

Focusing in Linear Meta-logic. - Vivek Nigam; Dale Miller 001 (IJCAR, 2008)

Canonical Sequent Proofs via Multi-Focusing. - Kaustuv Chaudhuri; Dale Miller 001; Alexis Saurin (IFIP TCS, 2008)

A Neutral Approach to Proof and Refutation in MALL. - Olivier Delande; Dale Miller 001 (LICS, 2008)

Combining Generic Judgments with Recursive Definitions. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (LICS, 2008)

Reasoning in Abella about Structural Operational Semantics Specifications. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (LFMTP@LICS, 2008)

Formalizing Operational Semantic Specifications in Logic. - Dale Miller 001 (WFLP, 2008)

A Unified Sequent Calculus for Focused Proofs. - Chuck C. Liang; Dale Miller 001 (LICS, 2009)

Algorithmic specifications in linear logic with subexponentials. - Vivek Nigam; Dale Miller 001 (PPDP, 2009)

Focusing and polarization in linear, intuitionistic, and classical logics. - Chuck C. Liang; Dale Miller 001 (Theor. Comput. Sci., 2009)

Reasoning about Computations Using Two-Levels of Logic. - Dale Miller 001 (APLAS, 2010)

Focused Inductive Theorem Proving. - David Baelde; Dale Miller 001; Zachary Snow (IJCAR, 2010)

Fixed Points and Proof Theory: An Extended Abstract. - Dale Miller 001 (FICS, 2010)

Proof and refutation in MALL as a game. - Olivier Delande; Dale Miller 001; Alexis Saurin (Ann. Pure Appl. Log., 2010)

A Framework for Proof Systems. - Vivek Nigam; Dale Miller 001 (J. Autom. Reason., 2010)

Proof search specifications of bisimulation and modal logics for the pi-calculus. - Alwen Tiu; Dale Miller 001 (ACM Trans. Comput. Log., 2010)

A Proposal for Broad Spectrum Proof Certificates. - Dale Miller 001 (CPP, 2011)

A focused approach to combining logics. - Chuck C. Liang; Dale Miller 001 (Ann. Pure Appl. Log., 2011)

Nominal abstraction. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (Inf. Comput., 2011)

Programming with Higher-Order Logic. - Dale Miller 001; Gopalan Nadathur (Cambridge University Press, 2012)

A Systematic Approach to Canonicity in the Classical Sequent Calculus. - Kaustuv Chaudhuri; Stefan Hetzl; Dale Miller 001 (CSL, 2012)

A non-local method for robustness analysis of floating point programs - Ivan Gazeau; Dale Miller 001; Catuscia Palamidessi (QAPL, 2012)

A Two-Level Logic Approach to Reasoning About Computations. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (J. Autom. Reason., 2012)

Foundational Proof Certificates in First-Order Logic. - Zakaria Chihani; Dale Miller 001; Fabien Renaud (CADE, 2013)

Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract). - Zakaria Chihani; Dale Miller 001; Fabien Renaud (PxTP@CADE, 2013)

Extracting Proofs from Tabled Proof Search. - Dale Miller 001; Alwen Tiu (CPP, 2013)

Foundational proof certificates: making proof universal and permanent. - Dale Miller 001 (LFMTP, 2013)

Unifying Classical and Intuitionistic Logics for Computational Control. - Chuck C. Liang; Dale Miller 001 (LICS, 2013)

Kripke semantics and proof systems for combining intuitionistic logic and classical logic. - Chuck C. Liang; Dale Miller 001 (Ann. Pure Appl. Log., 2013)

A formal framework for specifying sequent calculus proof systems. - Dale Miller 001; Elaine Pimentel (Theor. Comput. Sci., 2013)

Abella: A System for Reasoning about Relational Specifications. - David Baelde; Kaustuv Chaudhuri; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu; Yuting Wang 001 (J. Formaliz. Reason., 2014)

Automation of Higher-Order Logic. - Christoph Benzmüller; Dale Miller 001 (Computational Logic, 2014)

A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. - Kaustuv Chaudhuri; Matteo Cimini; Dale Miller 001 (CPP, 2015)

Defining the meaning of TPTP formatted proofs. - Roberto Blanco; Tomer Libal; Dale Miller 001 (IWIL@LPAR, 2015)

On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control. - Chuck C. Liang; Dale Miller 001 (LPAR, 2015)

Focused Labeled Proof Systems for Modal Logic. - Dale Miller 001; Marco Volpe 001 (LPAR, 2015)

Proof Outlines as Proof Certificates: A System Description. - Roberto Blanco; Dale Miller 001 (WoF'15, 2015)

A framework for proof certificates in finite state exploration. - Quentin Heath; Dale Miller 001 (PxTP@CADE, 2015)

Proof Certificates for Equality Reasoning. - Zakaria Chihani; Dale Miller 001 (LSFA, 2015)

A focused framework for emulating modal proof systems. - Sonia Marin; Dale Miller 001; Marco Volpe 001 (Advances in Modal Logic, 2016)

Functions-as-Constructors Higher-Order Unification. - Tomer Libal; Dale Miller 001 (FSCD, 2016)

Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). - Dale Miller 001 (TYPES, 2016)

Well-Typed Languages are Sound. - Matteo Cimini; Dale Miller 001; Jeremy G. Siek (CoRR, 2016)

A Proof Theory for Model Checking: An Extended Abstract. - Quentin Heath; Dale Miller 001 (LINEARITY, 2016)

A multi-focused proof system isomorphic to expansion proofs. - Kaustuv Chaudhuri; Stefan Hetzl; Dale Miller 001 (J. Log. Comput., 2016)

Preserving differential privacy under finite-precision semantics. - Ivan Gazeau; Dale Miller 001; Catuscia Palamidessi (Theor. Comput. Sci., 2016)

Translating Between Implicit and Explicit Versions of Proof. - Roberto Blanco; Zakaria Chihani; Dale Miller 001 (CADE, 2017)

Separating Functional Computation from Relations. - Ulysse Gérard; Dale Miller 001 (CSL, 2017)

Proof checking and logic programming. - Dale Miller 001 (Formal Aspects Comput., 2017)

A Semantic Framework for Proof Evidence. - Zakaria Chihani; Dale Miller 001; Fabien Renaud (J. Autom. Reason., 2017)

A proof-theoretic approach to certifying skolemization. - Kaustuv Chaudhuri; Matteo Manighetti; Dale Miller 001 (CPP, 2019)

Property-Based Testing via Proof Reconstruction. - Roberto Blanco; Dale Miller 001; Alberto Momigliano (PPDP, 2019)

Functional programming with λ-tree syntax. - Ulysse Gérard; Dale Miller 001; Gabriel Scherer (PPDP, 2019)

Functional programming with lambda-tree syntax. - Ulysse Gérard; Dale Miller 001; Gabriel Scherer (CoRR, 2019)

EATCS Distinguished Dissertation Award 2019 - Call for Nominations. - David Peleg; Susanne Albers; Elvira Mayordomo; Dale Miller 001; Jaroslav Nesetril; Damian Niwinski; Vladimiro Sassone (Bull. EATCS, 2019)

A Proof Theory for Model Checking. - Quentin Heath; Dale Miller 001 (J. Autom. Reason., 2019)

Mechanized Metatheory Revisited. - Dale Miller 001 (J. Autom. Reason., 2019)

Andre and the Early Days of Penn's Logic and Computation Group. - Dale Miller 001 (Logic, Language, and Security, 2020)

A Distributed and Trusted Web of Formal Proofs. - Dale Miller 001 (ICDCIT, 2020)

Extrinsically typed operational semantics for functional languages. - Matteo Cimini; Dale Miller 001; Jeremy G. Siek (SLE, 2020)

Two Applications of Logic Programming to Coq. - Matteo Manighetti; Dale Miller 001; Alberto Momigliano (TYPES, 2020)

EATCS Distinguished Dissertation Award 2020 - Call for Nominations. - Susanne Albers; Nikhil Bansal 001; Elvira Mayordomo; Dale Miller 001; Jaroslav Nesetril; Damian Niwinski; David Peleg; Vladimiro Sassone; Alexandra Silva 001 (Bull. EATCS, 2020)

Functions-as-constructors higher-order unification: extended pattern unification. - Tomer Libal; Dale Miller 001 (Ann. Math. Artif. Intell., 2022)

The undecidability of proof search when equality is a logical connective. - Dale Miller 001; Alexandre Viel (Ann. Math. Artif. Intell., 2022)

From axioms to synthetic inference rules via focusing. - Sonia Marin; Dale Miller 001; Elaine Pimentel; Marco Volpe 001 (Ann. Pure Appl. Log., 2022)

A Survey of the Proof-Theoretic Foundations of Logic Programming. - Dale Miller 001 (Theory Pract. Log. Program., 2022)

A Positive Perspective on Term Representation (Invited Talk). - Dale Miller 001; Jui-Hsuan Wu (CSL, 2023)

Formal Reasoning Using Distributed Assertions. - Farah Al Wardani; Kaustuv Chaudhuri; Dale Miller 001 (FroCoS, 2023)

A system of inference based on proof search: an extended abstract. - Dale Miller 001 (LICS, 2023)

Peano Arithmetic and μMALL. - Matteo Manighetti; Dale Miller 001 (CoRR, 2023)

Property-Based Testing by Elaborating Proof Outlines. - Dale Miller 001; Alberto Momigliano (Theory Pract. Log. Program., 2024)

About Trust and Proof: An Experimental Framework for Heterogeneous Verification. - Farah Al Wardani; Kaustuv Chaudhuri; Dale Miller 001 (The Practice of Formal Methods (II), 2024)

Linear Logic Using Negative Connectives. - Dale Miller 001 (FSCD, 2025)