Dale Miller
According to our database^{1},
Dale Miller
authored at least 122 papers
between 1982 and 2019.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at orcid.org

at dl.acm.org
On csauthors.net:
Bibliography
2019
A prooftheoretic approach to certifying skolemization.
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019
2017
A Semantic Framework for Proof Evidence.
J. Autom. Reasoning, 2017
Separating Functional Computation from Relations.
Proceedings of the 26th EACSL Annual Conference on Computer Science Logic, 2017
Translating Between Implicit and Explicit Versions of Proof.
Proceedings of the Automated Deduction  CADE 26, 2017
2016
A multifocused proof system isomorphic to expansion proofs.
J. Log. Comput., 2016
Proof Certificates for Equality Reasoning.
Electr. Notes Theor. Comput. Sci., 2016
A Proof Theory for Model Checking: An Extended Abstract.
Proceedings of the Proceedings Fourth International Workshop on Linearity, 2016
Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper).
Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016
FunctionsasConstructors HigherOrder Unification.
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016
A focused framework for emulating modal proof systems.
Proceedings of the Advances in Modal Logic 11, 2016
2015
A framework for proof certificates in finite state exploration.
Proceedings of the Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, 2015
Proof Outlines as Proof Certificates: A System Description.
Proceedings of the Proceedings First International Workshop on Focusing, 2015
Proof checking and logic programming.
Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, 2015
Focused Labeled Proof Systems for Modal Logic.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015
On Subexponentials, Synthetic Connectives, and Multilevel Delimited Control.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015
Defining the meaning of TPTP formatted proofs.
Proceedings of the IWIL@LPAR 2015, 2015
Proof Checking and Logic Programming.
Proceedings of the LogicBased Program Synthesis and Transformation, 2015
A Lightweight Formalization of the Metatheory of BisimulationUpTo.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015
2014
Automation of HigherOrder Logic.
Proceedings of the Computational Logic, 2014
Abella: A System for Reasoning about Relational Specifications.
J. Formalized Reasoning, 2014
2013
A formal framework for specifying sequent calculus proof systems.
Theor. Comput. Sci., 2013
Preserving differential privacy under finiteprecision semantics.
Proceedings of the Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, 2013
Kripke semantics and proof systems for combining intuitionistic logic and classical logic.
Ann. Pure Appl. Logic, 2013
Unifying Classical and Intuitionistic Logics for Computational Control.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013
Foundational proof certificates: making proof universal and permanent.
Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Metalanguages: Theory & Practice, 2013
Extracting Proofs from Tabled Proof Search.
Proceedings of the Certified Programs and Proofs  Third International Conference, 2013
Checking Foundational Proof Certificates for FirstOrder Logic (Extended Abstract).
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013
Foundational Proof Certificates in FirstOrder Logic.
Proceedings of the Automated Deduction  CADE24, 2013
2012
A TwoLevel Logic Approach to Reasoning About Computations.
J. Autom. Reasoning, 2012
A nonlocal method for robustness analysis of floating point programs
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.
Proceedings of the Computer Science Logic (CSL'12), 2012
Programming with HigherOrder Logic.
Cambridge University Press, ISBN: 9780521879408, 2012
2011
Nominal abstraction.
Inf. Comput., 2011
A focused approach to combining logics.
Ann. Pure Appl. Logic, 2011
A Proposal for Broad Spectrum Proof Certificates.
Proceedings of the Certified Programs and Proofs  First International Conference, 2011
2010
Proof search specifications of bisimulation and modal logics for the picalculus.
ACM Trans. Comput. Log., 2010
A Framework for Proof Systems.
J. Autom. Reasoning, 2010
Proof and refutation in MALL as a game.
Ann. Pure Appl. Logic, 2010
Fixed Points and Proof Theory: An Extended Abstract.
Proceedings of the 7th Workshop on Fixed Points in Computer Science, 2010
Focused Inductive Theorem Proving.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010
Reasoning about Computations Using TwoLevels of Logic.
Proceedings of the Programming Languages and Systems  8th Asian Symposium, 2010
2009
Focusing and polarization in linear, intuitionistic, and classical logics.
Theor. Comput. Sci., 2009
Formalizing Operational Semantic Specifications in Logic.
Electr. Notes Theor. Comput. Sci., 2009
Reasoning in Abella about Structural Operational Semantics Specifications.
Electr. Notes Theor. Comput. Sci., 2009
Algorithmic specifications in linear logic with subexponentials.
Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009
A Unified Sequent Calculus for Focused Proofs.
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009
2008
Formalizing Operational Semantic Specifications in Logic.
Bulletin of the EATCS, 2008
Combining Generic Judgments with Recursive Definitions.
Proceedings of the TwentyThird Annual IEEE Symposium on Logic in Computer Science, 2008
A Neutral Approach to Proof and Refutation in MALL.
Proceedings of the TwentyThird Annual IEEE Symposium on Logic in Computer Science, 2008
Canonical Sequent Proofs via MultiFocusing.
Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008
Focusing in Linear Metalogic.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008
2007
Least and Greatest Fixed Points in Linear Logic.
Proceedings of the Logic for Programming, 2007
From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic.
Proceedings of the Computer Science Logic, 21st International Workshop, 2007
Incorporating Tables into Proofs.
Proceedings of the Computer Science Logic, 21st International Workshop, 2007
Focusing and Polarization in Intuitionistic Logic.
Proceedings of the Computer Science Logic, 21st International Workshop, 2007
The Bedwyr System for Model Checking over Syntactic Expressions.
Proceedings of the Automated Deduction, 2007
2006
A Congruence Format for Namepassing Calculi.
Electr. Notes Theor. Comput. Sci., 2006
A Proof Theoretic Approach to Operational Semantics.
Electr. Notes Theor. Comput. Sci., 2006
Collection analysis for Horn clause programs.
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.
Proceedings of the Generative Programming and Component Engineering, 2006
Representing and Reasoning with Operational Semantics.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006
2005
A proof theory for generic judgments.
ACM Trans. Comput. Log., 2005
A Proof Search Specification of the piCalculus.
Electr. Notes Theor. Comput. Sci., 2005
On the Specification of Sequent Systems.
Proceedings of the Logic for Programming, 2005
A game semantics for proof search: preliminary results.
Proceedings of the Games for Logic and Programming Languages (GALOP 2005), 2005
2004
Bindings, Mobility of Bindings, and the "generic judgments"Quantifier: An Abstract.
Proceedings of the Computer Science Logic, 18th International Workshop, 2004
2003
Encoding transition systems in sequent calculus.
Theor. Comput. Sci., 2003
Encryption as an abstract data type.
Electr. Notes Theor. Comput. Sci., 2003
Reasoning about Proof Search Specifications: An Abstract.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003
A Proof Theory for Generic Judgments: An extended abstract.
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003
2002
Reasoning with higherorder abstract syntax in a logical framework.
ACM Trans. Comput. Log., 2002
Using Linear Logic to Reason about Sequent Systems.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2002
Encoding Generic Judgments.
Proceedings of the FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 2002
HigherOrder Quantification and Proof Search.
Proceedings of the Algebraic Methodology and Software Technology, 2002
2001
Encoding Generic Judgments: Preliminary results.
Electr. Notes Theor. Comput. Sci., 2001
2000
Cutelimination for a logic with definitions and induction.
Theor. Comput. Sci., 2000
Abstract Syntax for Variable Binders: An Overview.
Proceedings of the Computational Logic, 2000
1999
Foundational Aspects of Syntax.
ACM Comput. Surv., 1999
1997
A Logic for Reasoning with HigherOrder Abstract Syntax.
Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997
1996
Forum: A MultipleConclusion Specification Logic.
Theor. Comput. Sci., 1996
Encoding Transition Systems in Sequent Calculus.
Electr. Notes Theor. Comput. Sci., 1996
Logical Foundations for Open System Design.
ACM Comput. Surv., 1996
Linear Logic as Logic Programming: An Abstract.
Proceedings of the Logical Aspects of Computational Linguistics, 1996
1995
Observations about Using Logic as a Specification Language.
Proceedings of the 1995 Joint Conference on Declarative Programming, 1995
1994
Specifications Using MultipleConclusion Logic Programs.
Proceedings of the Programming Language Implementation and Logic Programming, 1994
A MultipleConclusion MetaLogic
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994
Specifications Using MultipleConclusion Logic Programs.
Proceedings of the Algebraic and Logic Programming, 4th International Conference, 1994
1993
A Proposal for Modules in LambdaProlog.
Proceedings of the Extensions of Logic Programming, 4th International Workshop, 1993
1992
From Operational Semantics for Abstract Machines.
Mathematical Structures in Computer Science, 1992
Unification Under a Mixed Prefix.
J. Symb. Comput., 1992
The piCalculus as a Theory in Linear Logic: Preliminary Results.
Proceedings of the Extensions of Logic Programming, Third International Workshop, 1992
1991
Uniform Proofs as a Foundation for Logic Programming.
Ann. Pure Appl. Logic, 1991
Abstract Syntax and Logic Programming.
Proceedings of the Logic Programming, First Russian Conference on Logic Programming, Irkutsk, Russia, September 1418, 1990, 1991
Logic Programming in a Fragment of Intuitionistic Linear Logic
Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991
Logics for Logic Programming: A Tutorial.
Proceedings of the Logic Programming, 1991
Unification of Simply Typed LamdaTerms as Logic Programming.
Proceedings of the Logic Programming, 1991
1990
HigherOrder Horn Clauses
J. ACM, October, 1990
From Operational Semantics to Abstract Machines: Preliminary Results.
LISP and Functional Programming, 1990
Extending Definite Clause Grammars with Scoping Constructs.
Proceedings of the Logic Programming, 1990
HigherOrder Logic Programming.
Proceedings of the Logic Programming, 1990
Representing Objects in a Logic Programming Langueage with Scoping Constructs.
Proceedings of the Logic Programming, 1990
Encoding a DependentType LambdaCalculus in a Logic Programming Language.
Proceedings of the 10th International Conference on Automated Deduction, 1990
Tutorial on LambdaProlog.
Proceedings of the 10th International Conference on Automated Deduction, 1990
1989
A Logical Analysis of Modules in Logic Programming.
J. Log. Program., 1989
Deriving Mixed Evaluation from Standard Evaluation for a Simple Functional Language.
Proceedings of the Mathematics of Program Construction, 1989
Lexical Scoping as Universal Quantification.
Proceedings of the Logic Programming, 1989
A Logic Programming Language with LambdaAbstraction, Function Variables, and Simple Unification.
Proceedings of the Extensions of Logic Programming, 1989
1988
A MetaLogic for Functional Programming.
META, 1988
An Overview of LambdaPROLOG.
Proceedings of the Logic Programming, 1988
Uses of HigherOrder Unification for Implementing Program Transformers.
Proceedings of the Logic Programming, 1988
Specifying Theorem Provers in a HigherOrder Logic Programming Language.
Proceedings of the 9th International Conference on Automated Deduction, 1988
LambdaProlog: An Extended Logic Programming Language.
Proceedings of the 9th International Conference on Automated Deduction, 1988
1987
A compact representation of proofs.
Studia Logica, 1987
A Logic Programming Approach to Manipulating Formulas and Programs.
Proceedings of the 1987 Symposium on Logic Programming, San Francisco, California, USA, August 31, 1987
Hereditary Harrop Formulas and Uniform Proof Systems
Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987
1986
A Theory of Modules for Logic Programming.
Proceedings of the 1986 Symposium on Logic Programming, 1986
HigherOrder Logic Programming.
Proceedings of the Third International Conference on Logic Programming, 1986
Research in Natural Language Processing.
Proceedings of the Strategic Computing, 1986
Some Uses of HigherOrder Logic in Computational Linguistics.
Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, 1986
An Integration of Resolution and Natural Deduction Theorem Proving.
Proceedings of the 5th National Conference on Artificial Intelligence. Philadelphia, 1986
1984
Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs.
Proceedings of the 7th International Conference on Automated Deduction, 1984
1982
A Look at TPS.
Proceedings of the 6th Conference on Automated Deduction, 1982