Dale Miller

According to our database, Dale Miller authored at least 140 papers between 1982 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2023

Peano Arithmetic and μMALL.

Matteo Manighetti, Dale Miller

CoRR, 2023

A system of inference based on proof search: an extended abstract.

Dale Miller

LICS, 2023

Formal Reasoning Using Distributed Assertions.

Farah Al Wardani, Kaustuv Chaudhuri, Dale Miller

Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

A Positive Perspective on Term Representation (Invited Talk).

Dale Miller, Jui-Hsuan Wu

Proceedings of the 31st EACSL Annual Conference on Computer Science Logic, 2023

2022

A Survey of the Proof-Theoretic Foundations of Logic Programming.

Dale Miller

Theory Pract. Log. Program., 2022

From axioms to synthetic inference rules via focusing.

Sonia Marin, Dale Miller, Elaine Pimentel, Marco Volpe

Ann. Pure Appl. Log., 2022

The undecidability of proof search when equality is a logical connective.

Dale Miller, Alexandre Viel

Ann. Math. Artif. Intell., 2022

Functions-as-constructors higher-order unification: extended pattern unification.

Tomer Libal, Dale Miller

Ann. Math. Artif. Intell., 2022

2020

EATCS Distinguished Dissertation Award 2020 - Call for Nominations.

Susanne Albers, Nikhil Bansal, Elvira Mayordomo, Dale Miller, Jaroslav Nesetril, Damian Niwinski, David Peleg, Vladimiro Sassone, Alexandra Silva

Bull. EATCS, 2020

Two Applications of Logic Programming to Coq.

Matteo Manighetti, Dale Miller, Alberto Momigliano

Proceedings of the 26th International Conference on Types for Proofs and Programs, 2020

Extrinsically typed operational semantics for functional languages.

Matteo Cimini, Dale Miller, Jeremy G. Siek

Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, 2020

A Distributed and Trusted Web of Formal Proofs.

Dale Miller

Proceedings of the Distributed Computing and Internet Technology, 2020

Andre and the Early Days of Penn's Logic and Computation Group.

Dale Miller

Proceedings of the Logic, 2020

2019

Mechanized Metatheory Revisited.

Dale Miller

J. Autom. Reason., 2019

A Proof Theory for Model Checking.

Quentin Heath, Dale Miller

J. Autom. Reason., 2019

EATCS Distinguished Dissertation Award 2019 - Call for Nominations.

David Peleg, Susanne Albers, Elvira Mayordomo, Dale Miller, Jaroslav Nesetril, Damian Niwinski, Vladimiro Sassone

Bull. EATCS, 2019

Functional programming with lambda-tree syntax.

Ulysse Gérard, Dale Miller, Gabriel Scherer

CoRR, 2019

Functional programming with λ-tree syntax.

Ulysse Gérard, Dale Miller, Gabriel Scherer

Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, 2019

Property-Based Testing via Proof Reconstruction.

Roberto Blanco, Dale Miller, Alberto Momigliano

Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, 2019

A proof-theoretic approach to certifying skolemization.

Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2017

A Semantic Framework for Proof Evidence.

Zakaria Chihani, Dale Miller, Fabien Renaud

J. Autom. Reason., 2017

Proof checking and logic programming.

Dale Miller

Formal Aspects Comput., 2017

Separating Functional Computation from Relations.

Ulysse Gérard, Dale Miller

Proceedings of the 26th EACSL Annual Conference on Computer Science Logic, 2017

Translating Between Implicit and Explicit Versions of Proof.

Roberto Blanco, Zakaria Chihani, Dale Miller

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Preserving differential privacy under finite-precision semantics.

Ivan Gazeau, Dale Miller, Catuscia Palamidessi

Theor. Comput. Sci., 2016

A multi-focused proof system isomorphic to expansion proofs.

Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller

J. Log. Comput., 2016

A Proof Theory for Model Checking: An Extended Abstract.

Quentin Heath, Dale Miller

Proceedings of the Proceedings Fourth International Workshop on Linearity, 2016

Well-Typed Languages are Sound.

Matteo Cimini, Dale Miller, Jeremy G. Siek

CoRR, 2016

Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper).

Dale Miller

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

Functions-as-Constructors Higher-Order Unification.

Tomer Libal, Dale Miller

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

A focused framework for emulating modal proof systems.

Sonia Marin, Dale Miller, Marco Volpe

Proceedings of the Advances in Modal Logic 11, 2016

2015

Proof Certificates for Equality Reasoning.

Zakaria Chihani, Dale Miller

Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

A framework for proof certificates in finite state exploration.

Quentin Heath, Dale Miller

Proceedings of the Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, 2015

Proof Outlines as Proof Certificates: A System Description.

Roberto Blanco, Dale Miller

Proceedings of the Proceedings First International Workshop on Focusing, 2015

Focused Labeled Proof Systems for Modal Logic.

Dale Miller, Marco Volpe

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control.

Chuck C. Liang, Dale Miller

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Defining the meaning of TPTP formatted proofs.

Roberto Blanco, Tomer Libal, Dale Miller

Proceedings of the IWIL@LPAR 2015, 2015

A Lightweight Formalization of the Metatheory of Bisimulation-Up-To.

Kaustuv Chaudhuri, Matteo Cimini, Dale Miller

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014

Automation of Higher-Order Logic.

Christoph Benzmüller, Dale Miller

Proceedings of the Computational Logic, 2014

Abella: A System for Reasoning about Relational Specifications.

David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang

J. Formaliz. Reason., 2014

2013

A formal framework for specifying sequent calculus proof systems.

Dale Miller, Elaine Pimentel

Theor. Comput. Sci., 2013

Kripke semantics and proof systems for combining intuitionistic logic and classical logic.

Chuck C. Liang, Dale Miller

Ann. Pure Appl. Log., 2013

Unifying Classical and Intuitionistic Logics for Computational Control.

Chuck C. Liang, Dale Miller

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Foundational proof certificates: making proof universal and permanent.

Dale Miller

Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, 2013

Extracting Proofs from Tabled Proof Search.

Dale Miller, Alwen Tiu

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract).

Zakaria Chihani, Dale Miller, Fabien Renaud

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

Foundational Proof Certificates in First-Order Logic.

Zakaria Chihani, Dale Miller, Fabien Renaud

Proceedings of the Automated Deduction - CADE-24, 2013

2012

A Two-Level Logic Approach to Reasoning About Computations.

Andrew Gacek, Dale Miller, Gopalan Nadathur

J. Autom. Reason., 2012

A non-local method for robustness analysis of floating point programs

Ivan Gazeau, Dale Miller, Catuscia Palamidessi

Proceedings of the Proceedings 10th Workshop on Quantitative Aspects of Programming Languages and Systems, 2012

A Systematic Approach to Canonicity in the Classical Sequent Calculus.

Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller

Proceedings of the Computer Science Logic (CSL'12), 2012

Programming with Higher-Order Logic.

Dale Miller, Gopalan Nadathur

Cambridge University Press, ISBN: 978-0-521-87940-8, 2012

2011

Nominal abstraction.

Andrew Gacek, Dale Miller, Gopalan Nadathur

Inf. Comput., 2011

A focused approach to combining logics.

Chuck C. Liang, Dale Miller

Ann. Pure Appl. Log., 2011

A Proposal for Broad Spectrum Proof Certificates.

Dale Miller

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Proof search specifications of bisimulation and modal logics for the pi-calculus.

Alwen Tiu, Dale Miller

ACM Trans. Comput. Log., 2010

A Framework for Proof Systems.

Vivek Nigam, Dale Miller

J. Autom. Reason., 2010

Proof and refutation in MALL as a game.

Olivier Delande, Dale Miller, Alexis Saurin

Ann. Pure Appl. Log., 2010

Fixed Points and Proof Theory: An Extended Abstract.

Dale Miller

Proceedings of the 7th Workshop on Fixed Points in Computer Science, 2010

Focused Inductive Theorem Proving.

David Baelde, Dale Miller, Zachary Snow

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

Reasoning about Computations Using Two-Levels of Logic.

Dale Miller

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009

Focusing and polarization in linear, intuitionistic, and classical logics.

Chuck C. Liang, Dale Miller

Theor. Comput. Sci., 2009

Algorithmic specifications in linear logic with subexponentials.

Vivek Nigam, Dale Miller

Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

A Unified Sequent Calculus for Focused Proofs.

Chuck C. Liang, Dale Miller

Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

2008

Formalizing Operational Semantic Specifications in Logic.

Dale Miller

Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming, 2008

Reasoning in Abella about Structural Operational Semantics Specifications.

Andrew Gacek, Dale Miller, Gopalan Nadathur

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

Combining Generic Judgments with Recursive Definitions.

Andrew Gacek, Dale Miller, Gopalan Nadathur

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

A Neutral Approach to Proof and Refutation in MALL.

Olivier Delande, Dale Miller

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

Canonical Sequent Proofs via Multi-Focusing.

Kaustuv Chaudhuri, Dale Miller, Alexis Saurin

Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

Focusing in Linear Meta-logic.

Vivek Nigam, Dale Miller

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

Least and Greatest Fixed Points in Linear Logic.

David Baelde, Dale Miller

Proceedings of the Logic for Programming, 2007

From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic.

Dale Miller, Alexis Saurin

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

Incorporating Tables into Proofs.

Dale Miller, Vivek Nigam

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

Focusing and Polarization in Intuitionistic Logic.

Chuck C. Liang, Dale Miller

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

The Bedwyr System for Model Checking over Syntactic Expressions.

David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu

Proceedings of the Automated Deduction, 2007

2006

Collection analysis for Horn clause programs.

Dale Miller

Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 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, Simon L. Peyton Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump

Proceedings of the Generative Programming and Component Engineering, 2006

Representing and Reasoning with Operational Semantics.

Dale Miller

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

A proof theory for generic judgments.

Dale Miller, Alwen Tiu

ACM Trans. Comput. Log., 2005

A Congruence Format for Name-passing Calculi.

Axelle Ziegler, Dale Miller, Catuscia Palamidessi

Proceedings of the Second Workshop on Structural Operational Semantics, 2005

A Game Semantics for Proof Search: Preliminary Results.

Dale Miller, Alexis Saurin

Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics, 2005

A Proof Theoretic Approach to Operational Semantics.

Dale Miller

Proceedings of the Workshop "Essays on Algebraic Process Calculi", 2005

On the Specification of Sequent Systems.

Elaine Pimentel, Dale Miller

Proceedings of the Logic for Programming, 2005

2004

A Proof Search Specification of the pi-Calculus.

Alwen Fernanto Tiu, Dale Miller

Proceedings of the Workshop 3rd on the Foundations of Global Ubiquitous Computing, 2004

Bindings, Mobility of Bindings, and the "generic judgments"-Quantifier: An Abstract.

Dale Miller

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

2003

Encryption as an abstract data type.

Dale Miller

Proceedings of the 10th Workshop on Logic, Language, Information and Computation, 2003

Reasoning about Proof Search Specifications: An Abstract.

Dale Miller

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

A Proof Theory for Generic Judgments: An extended abstract.

Dale Miller, Alwen Fernanto Tiu

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

2002

Reasoning with higher-order abstract syntax in a logical framework.

Raymond McDowell, Dale Miller

ACM Trans. Comput. Log., 2002

Using Linear Logic to Reason about Sequent Systems.

Dale Miller, Elaine Pimentel

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2002

Encoding Generic Judgments.

Dale Miller, Alwen Fernanto Tiu

Proceedings of the FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 2002

Higher-Order Quantification and Proof Search.

Dale Miller

Proceedings of the Algebraic Methodology and Software Technology, 2002

2001

Encoding Generic Judgments: Preliminary results.

Dale Miller

Proceedings of the Mechanized Reasoning about Languages with Variable Binding, 2001

2000

Cut-elimination for a logic with definitions and induction.

Raymond McDowell, Dale Miller

Theor. Comput. Sci., 2000

Abstract Syntax for Variable Binders: An Overview.

Dale Miller

Proceedings of the Computational Logic, 2000

1999

Foundational Aspects of Syntax.

Dale Miller, Catuscia Palamidessi

ACM Comput. Surv., 1999

1997

A Logic for Reasoning with Higher-Order Abstract Syntax.

Raymond McDowell, Dale Miller

Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997

1996

Forum: A Multiple-Conclusion Specification Logic.

Dale Miller

Theor. Comput. Sci., 1996

Encoding Transition Systems in Sequent Calculus.

Raymond McDowell, Dale Miller, Catuscia Palamidessi

Proceedings of the Linear Logic Tokyo Meeting 1996, Keio University, Mita Campus, Tokyo, Japan, March 29, 1996

Logical Foundations for Open System Design.

Dale Miller

ACM Comput. Surv., 1996

Linear Logic as Logic Programming: An Abstract.

Dale Miller

Proceedings of the Logical Aspects of Computational Linguistics, 1996

1995

Observations about Using Logic as a Specification Language.

Dale Miller

Proceedings of the 1995 Joint Conference on Declarative Programming, 1995

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

Designing User Interfaces for Hypermedia, 1995

1994

Logic Programming in a Fragment of Intuitionistic Linear Logic

Joshua S. Hodas, Dale Miller

Inf. Comput., May, 1994

A Multiple-Conclusion Meta-Logic

Dale Miller

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Specifications Using Multiple-Conclusion Logic Programs.

Dale Miller

Proceedings of the Algebraic and Logic Programming, 4th International Conference, 1994

1993

A Proposal for Modules in Lambda-Prolog.

Dale Miller

Proceedings of the Extensions of Logic Programming, 4th International Workshop, 1993

1992

From Operational Semantics for Abstract Machines.

John Hannan, Dale Miller

Math. Struct. Comput. Sci., 1992

Unification Under a Mixed Prefix.

Dale Miller

J. Symb. Comput., 1992

The pi-Calculus as a Theory in Linear Logic: Preliminary Results.

Dale Miller

Proceedings of the Extensions of Logic Programming, Third International Workshop, 1992

Flexible Diff-ing in a Collaborative Writing System.

Christine Neuwirth, Ravinder Chandhok, David Kaufer, Paul Erion, James H. Morris, Dale Miller

Proceedings of the CSCW '92, Proceedings of the Conference on Computer Supported Cooperative Work, Toronto, Canada, October 31, 1992

1991

A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification.

Dale Miller

J. Log. Comput., 1991

Uniform Proofs as a Foundation for Logic Programming.

Dale Miller, Gopalan Nadathur, Frank Pfenning, Andre Scedrov

Ann. Pure Appl. Log., 1991

Abstract Syntax and Logic Programming.

Dale Miller

Proceedings of the Logic Programming, First Russian Conference on Logic Programming, Irkutsk, Russia, September 14-18, 1990, 1991

Logics for Logic Programming: A Tutorial.

Dale Miller

Proceedings of the Logic Programming, 1991

Unification of Simply Typed Lamda-Terms as Logic Programming.

Dale Miller

Proceedings of the Logic Programming, 1991

1990

Higher-Order Horn Clauses

Gopalan Nadathur, Dale Miller

J. ACM, October, 1990

From Operational Semantics to Abstract Machines: Preliminary Results.

John Hannan, Dale Miller

Proceedings of the 1990 ACM Conference on LISP and Functional Programming, 1990

Extending Definite Clause Grammars with Scoping Constructs.

Remo Pareschi, Dale Miller

Proceedings of the Logic Programming, 1990

Higher-Order Logic Programming.

Dale Miller

Proceedings of the Logic Programming, 1990

Representing Objects in a Logic Programming Langueage with Scoping Constructs.

Joshua S. Hodas, Dale Miller

Proceedings of the Logic Programming, 1990

Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language.

Amy P. Felty, Dale Miller

Proceedings of the 10th International Conference on Automated Deduction, 1990

Tutorial on Lambda-Prolog.

Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning

Proceedings of the 10th International Conference on Automated Deduction, 1990

1989

A Logical Analysis of Modules in Logic Programming.

Dale Miller

J. Log. Program., 1989

Deriving Mixed Evaluation from Standard Evaluation for a Simple Functional Language.

John Hannan, Dale Miller

Proceedings of the Mathematics of Program Construction, 1989

Lexical Scoping as Universal Quantification.

Dale Miller

Proceedings of the Logic Programming, 1989

1988

A Meta-Logic for Functional Programming.

John Hannan, Dale Miller

Proceedings of the Meta-Programming in Logic Programming, 1988

An Overview of Lambda-PROLOG.

Gopalan Nadathur, Dale Miller

Proceedings of the Logic Programming, 1988

Uses of Higher-Order Unification for Implementing Program Transformers.

John Hannan, Dale Miller

Proceedings of the Logic Programming, 1988

Specifying Theorem Provers in a Higher-Order Logic Programming Language.

Amy P. Felty, Dale Miller

Proceedings of the 9th International Conference on Automated Deduction, 1988

Lambda-Prolog: An Extended Logic Programming Language.

Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov

Proceedings of the 9th International Conference on Automated Deduction, 1988

1987

A compact representation of proofs.

Dale A. Miller

Stud Logica, 1987

A Logic Programming Approach to Manipulating Formulas and Programs.

Dale Miller, Gopalan Nadathur

Proceedings of the 1987 Symposium on Logic Programming, San Francisco, California, USA, August 31, 1987

Hereditary Harrop Formulas and Uniform Proof Systems

Dale Miller, Gopalan Nadathur, Andre Scedrov

Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

1986

A Theory of Modules for Logic Programming.

Dale Miller

Proceedings of the 1986 Symposium on Logic Programming, 1986

Higher-Order Logic Programming.

Dale Miller, Gopalan Nadathur

Proceedings of the Third International Conference on Logic Programming, 1986

Research in Natural Language Processing.

Aravind K. Joshi, Timothy W. Finin, Dale Miller, Lokendra Shastri, Bonnie L. Webber

Proceedings of the Strategic Computing, 1986

Some Uses of Higher-Order Logic in Computational Linguistics.

Dale Miller, Gopalan Nadathur

Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, 1986

An Integration of Resolution and Natural Deduction Theorem Proving.

Dale Miller, Amy P. Felty

Proceedings of the 5th National Conference on Artificial Intelligence. Philadelphia, 1986

1984

Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs.

Dale Miller

Proceedings of the 7th International Conference on Automated Deduction, 1984

1982

A Look at TPS.

Dale A. Miller, Eve Longini Cohen, Peter B. Andrews

Proceedings of the 6th Conference on Automated Deduction, 1982