Dale Miller

According to our database1, Dale Miller authored at least 122 papers between 1982 and 2019.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
A proof-theoretic 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 multi-focused 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

Functions-as-Constructors Higher-Order 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 Multi-level 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 Logic-Based Program Synthesis and Transformation, 2015

A Lightweight Formalization of the Metatheory of Bisimulation-Up-To.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014
Automation of Higher-Order 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 finite-precision 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 & Meta-languages: 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 First-Order Logic (Extended Abstract).
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

Foundational Proof Certificates in First-Order Logic.
Proceedings of the Automated Deduction - CADE-24, 2013

2012
A Two-Level Logic Approach to Reasoning About Computations.
J. Autom. Reasoning, 2012

A non-local 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 Higher-Order Logic.
Cambridge University Press, ISBN: 978-0-521-87940-8, 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 pi-calculus.
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 Two-Levels 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 Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

A Neutral Approach to Proof and Refutation in MALL.
Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

Canonical Sequent Proofs via Multi-Focusing.
Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

Focusing in Linear Meta-logic.
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 Name-passing 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 pi-Calculus.
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 higher-order 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

Higher-Order 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
Cut-elimination 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 Higher-Order Abstract Syntax.
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.
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 Multiple-Conclusion Logic Programs.
Proceedings of the Programming Language Implementation and Logic Programming, 1994

A Multiple-Conclusion Meta-Logic
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Specifications Using Multiple-Conclusion Logic Programs.
Proceedings of the Algebraic and Logic Programming, 4th International Conference, 1994

1993
A Proposal for Modules in Lambda-Prolog.
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 pi-Calculus 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 14-18, 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 Lamda-Terms as Logic Programming.
Proceedings of the Logic Programming, 1991

1990
Higher-Order 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

Higher-Order 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 Dependent-Type Lambda-Calculus in a Logic Programming Language.
Proceedings of the 10th International Conference on Automated Deduction, 1990

Tutorial on Lambda-Prolog.
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 Lambda-Abstraction, Function Variables, and Simple Unification.
Proceedings of the Extensions of Logic Programming, 1989

1988
A Meta-Logic for Functional Programming.
META, 1988

An Overview of Lambda-PROLOG.
Proceedings of the Logic Programming, 1988

Uses of Higher-Order Unification for Implementing Program Transformers.
Proceedings of the Logic Programming, 1988

Specifying Theorem Provers in a Higher-Order Logic Programming Language.
Proceedings of the 9th International Conference on Automated Deduction, 1988

Lambda-Prolog: 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

Higher-Order 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 Higher-Order 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


  Loading...