Dale Miller, Alexandre Viel. The undecidability of proof search when equality is a logical connective. Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2021, ⟨10.1007/s10472-021-09764-0⟩. ⟨hal-03457312⟩

Tomer Libal, Dale Miller. Functions-as-constructors higher-order unification: extended pattern unification. Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2021, ⟨10.1007/s10472-021-09774-y⟩. ⟨hal-03457303⟩

Dale Miller. Reciprocal Influences Between Proof Theory and Logic Programming. Philosophy & Technology, Springer, 2021, 34, pp.75-104. ⟨10.1007/s13347-019-00370-x⟩. ⟨hal-02368867⟩

Dale Miller. A Survey of the Proof-Theoretic Foundations of Logic Programming. Theory and Practice of Logic Programming, Cambridge University Press (CUP), 2021, pp.1-46. ⟨10.1017/S1471068421000533⟩. ⟨hal-03411144⟩

Dale Miller. Mechanized metatheory revisited. Journal of Automated Reasoning, Springer Verlag, 2019, 63 (3), pp.625-665. ⟨10.1007/s10817-018-9483-3⟩. ⟨hal-01884210⟩

Quentin Heath, Dale Miller. A proof theory for model checking. Journal of Automated Reasoning, Springer Verlag, 2019, 63 (4), pp.857-885. ⟨10.1007/s10817-018-9475-3⟩. ⟨hal-01814006⟩

Zakaria Chihani, Dale Miller, Fabien Renaud. A Semantic Framework for Proof Evidence. Journal of Automated Reasoning, Springer Verlag, 2017, 59 (3), pp.287-330. ⟨10.1007/s10817-016-9380-6⟩. ⟨hal-01390912⟩

Zakaria Chihani, Dale Miller. Proof Certificates for Equality Reasoning. Electronic Notes in Theoretical Computer Science, Elsevier, 2016, 323, pp.93 - 108. ⟨10.1016/j.entcs.2016.06.007⟩. ⟨hal-01390919⟩

Ivan Gazeau, Dale Miller, Catuscia Palamidessi. Preserving differential privacy under finite-precision semantics. Theoretical Computer Science, Elsevier, 2016. ⟨hal-01390927⟩

Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. A Multi-Focused Proof System Isomorphic to Expansion Proofs. Journal of Logic and Computation, Oxford University Press (OUP), 2014. ⟨hal-00937056⟩

David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, et al.. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, Special Issue: User Tutorials 2, 7 (2), pp.1-89. ⟨10.6092/issn.1972-5787/4650⟩. ⟨hal-01102709⟩

Chuck Liang, Dale Miller. Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic. Annals of Pure and Applied Logic, Elsevier Masson, 2013, 164 (2), pp.86-111. ⟨10.1016/j.apal.2012.09.005⟩. ⟨hal-00787601⟩

Dale Miller, Elaine Pimentel. A formal framework for specifying sequent calculus proof systems. Theoretical Computer Science, Elsevier, 2013, pp.98-116. ⟨10.1016/j.tcs.2012.12.008⟩. ⟨hal-00787586⟩

Andrew Gacek, Dale Miller, Gopalan Nadathur. A two-level logic approach to reasoning about computations. Journal of Automated Reasoning, Springer Verlag, 2012, 49 (2), pp.241-273. ⟨10.1007/s10817-011-9218-1⟩. ⟨hal-00776208⟩

Chuck Liang, Dale Miller. A Focused Approach to Combining Logics. Annals of Pure and Applied Logic, Elsevier Masson, 2011, ⟨10.1016/j.apal.2011.01.012⟩. ⟨hal-00772736⟩

Gacek Andrew, Dale Miller, Gopalan Nadathur. Nominal Abstraction. Information and Computation, Elsevier, 2011, 209 (1), pp.48-73. ⟨hal-00772606⟩

Olivier Delande, Dale Miller, Alexis Saurin. Proof and Refutation in MALL as a game. Annals of Pure and Applied Logic, Elsevier Masson, 2010, 161 (5), pp.654-672. ⟨10.1016/j.apal.2009.07.017⟩. ⟨hal-00527922⟩

Tiu Alwen, Dale Miller. Proof Search Specifications of the pi-calculus. ACM Transactions on Computational Logic, Association for Computing Machinery, 2010, 11 (2). ⟨hal-00772571⟩

Nigam Vivek, Dale Miller. A framework for proof systems. Journal of Automated Reasoning, Springer Verlag, 2010, 45 (2). ⟨hal-00772562⟩

Chuck Liang, Dale Miller. Focusing and Polarization in Linear, Intuitionistic, and Classical Logics. Theoretical Computer Science, Elsevier, 2009, 410 (46), ⟨10.1016/j.tcs.2009.07.041⟩. ⟨hal-00772342⟩

Dale Miller. A Distributed and Trusted Web of Formal Proofs. ICDCIT 2020 - 16th International Conference on Distributed Computing and Internet Technology, Jan 2020, Bhubaneswar, India. pp.21-40, ⟨10.1007/978-3-030-36987-3_2⟩. ⟨hal-02468229⟩

Matteo Manighetti, Dale Miller, Alberto Momigliano. Two Applications of Logic Programming to Coq. 26th International Conference on Types for Proofs and Programs (TYPES 2020), Mar 2020, Turin, Italy. ⟨hal-03457352⟩

Ulysse Gérard, Dale Miller, Gabriel Scherer. Functional programming with $λ$-tree syntax. PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-16, ⟨10.1145/3354166.3354177⟩. ⟨hal-02368906⟩

Roberto Blanco, Dale Miller, Alberto Momigliano. Property-Based Testing via Proof Reconstruction. PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-13, ⟨10.1145/3354166.3354170⟩. ⟨hal-02368931⟩

Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller. A Proof-Theoretic Approach to Certifying Skolemization. CPP 2019 - 8th ACM SIGPLAN International Conference, Jan 2019, Cascais, Portugal. pp.78-90, ⟨10.1145/3293880.3294094⟩. ⟨hal-02368946⟩

Ulysse Gérard, Dale Miller. Functional programming with λ$-tree$ syntax: a progress report. 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2018, Oxford, United Kingdom. ⟨hal-01806129v2⟩

Kaustuv Chaudhuri, Ulysse Gérard, Dale Miller. Computation-as-deduction in Abella: work in progress. 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2018, Oxford, United Kingdom. ⟨hal-01806154⟩

Dale Miller. Using linear logic and proof theory to unify computational logic. Proceedings of Trends in Linear Logic and Applications (TLLA 17), Sep 2017, Oxford, United Kingdom. ⟨hal-01615673⟩

Roberto Blanco, Dale Miller, Alberto Momigliano. Property-Based Testing via Proof Reconstruction Work-in-progress. LFMTP 17: Logical Frameworks and Meta-Languages: Theory and Practice, Sep 2017, Oxford, United Kingdom. ⟨hal-01646788⟩

Ulysse Gérard, Dale Miller. Separating Functional Computation from Relations. 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. pp.23:1--23:17. ⟨hal-01615683⟩

Roberto Blanco, Zakaria Chihani, Dale Miller. Translating Between Implicit and Explicit Versions of Proof. CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. ⟨hal-01645016⟩

Dale Miller. Linear logic as a logical framework. Proceedings of Structures and Deduction (SD) 2017, Sep 2017, Oxford, United Kingdom. ⟨hal-01615664⟩

Dale Miller. Mechanized Metatheory Revisited: An Extended Abstract . Post-proceedings of TYPES 2016 , 2017, Novi Sad, Serbia. ⟨10.4230/LIPIcs⟩. ⟨hal-01615681⟩

Tomer Libal, Dale Miller. Functions-as-constructors Higher-order Unification. 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Delia Kesner and Brigitte Pientka, Jun 2016, Porto, Portugal. pp.1 - 17, ⟨10.4230/LIPIcs.FSCD.2016.26⟩. ⟨hal-01379683⟩

Sonia Marin, Dale Miller, Marco Volpe. A focused framework for emulating modal proof systems. 11th conference on "Advances in Modal Logic", Aug 2016, Budapest, Hungary. pp.469-488. ⟨hal-01379624⟩

Roberto Blanco, Tomer Libal, Dale Miller. Defining the meaning of TPTP formatted proofs. 11th International Workshop on the Implementation of Logics, Nov 2015, Suva, Fiji. ⟨hal-01238434⟩

Chuck Liang, Dale Miller. On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control. LPAR 20 - International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp.297-312, ⟨10.1007/978-3-662-48899-7_21⟩. ⟨hal-01239753⟩

Dale Miller, Marco Volpe. Focused labeled proof systems for modal logic. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji. ⟨hal-01213858⟩

Quentin Heath, Dale Miller. A framework for proof certificates in finite state exploration. Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, Aug 2015, Berlin, Germany. ⟨10.4204/EPTCS.186.4⟩. ⟨hal-01240172⟩

Kaustuv Chaudhuri, Matteo Cimini, Dale Miller. A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP), ACM-SIGPLAN, Jan 2015, Mumbai, India. ⟨10.1145/2676724.2693170⟩. ⟨hal-01091524⟩

Roberto Blanco, Dale Miller. Proof Outlines as Proof Certificates: A System Description. First International Workshop on Focusing, Nov 2015, Suva, Fiji. ⟨hal-01238436⟩

Zakaria Chihani, Dale Miller, Fabien Renaud. Foundational proof certificates in first-order logic. CADE - 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, United States. ⟨hal-00906485⟩

Chuck Liang, Dale Miller. Unifying Classical and Intuitionistic Logics for Computational Control. LOGIC IN COMPUTER SCIENCE (LICS 2013), Jun 2013, New Orleans, United States. ⟨hal-00906299⟩

Zakaria Chihani, Dale Miller, Fabien Renaud. Checking foundational proof certificates for first-order logic. PxTP - Proof Exchange for Theorem Proving, Jun 2013, Lake Placid, United States. ⟨hal-00906486⟩

Ivan Gazeau, Dale Miller, Catuscia Palamidessi. Preserving differential privacy under finite-precision semantics. QAPL - 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, Mar 2013, Rome, Italy. pp.1-18, ⟨10.4204/EPTCS.117.1⟩. ⟨hal-00780774v2⟩

Ivan Gazeau, Dale Miller, Catuscia Palamidessi. A non-local method for robustness analysis of floating point programs. QAPL - Tenth Workshop on Quantitative Aspects of Programming Languages, Mar 2012, Tallinn, Estonia. pp.63-76, ⟨10.4204/EPTCS.85.5⟩. ⟨hal-00665995v3⟩

Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. 21st EACSL Annual Conference on Computer Science Logic, Sep 2012, Fontainebleau, France. pp.183-197, ⟨10.4230/LIPIcs.CSL.2012.183⟩. ⟨hal-00772396⟩

Dale Miller. A proposal for broad spectrum proof certificates. CPP 2011 - First International Conference on Certified Proofs and Programs, 2011, Kenting, Taiwan. ⟨hal-00772722⟩

Dale Miller, Arnaud Carayol, Panos Rondogiannis, Lars Birkedal, Marek Czarnecki, et al.. FICS 2010. 7th Workshop on Fixed Points in Computer Science, FICS 2010, Aug 2010, Brno, Czech Republic. pp.89. ⟨hal-00512377⟩

Dale Miller. Finding Unity in Computational Logic. ACM-BCS Visions of Computer Science, 2010, Edinburgh, United Kingdom. ⟨hal-00772557⟩

Dale Miller. Reasoning about computations using two-levels of logic. APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems, 2010, Shanghai, China. ⟨hal-00772599⟩

David Baelde, Dale Miller, Zachary Snow. Focused Inductive Theorem Proving. IJCAR 2010 - International Joint Conference on Automated Deduction, 2010, Edinburgh, United Kingdom. ⟨hal-00772592⟩

Nigam Vivek, Dale Miller. Algorithmic specifications in linear logic with subexponentials. PPDP09 - ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Sep 2009, Coimbra, Portugal. ⟨hal-00772332⟩

Liang Chuck, Dale Miller. A Unified Sequent Calculus for Focused Proofs. LICS 2009 - Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE, Aug 2009, Los Angeles, United States. ⟨hal-00772347⟩

Alexis Saurin, Kaustuv C. Chaudhuri, Dale Miller. Canonical Sequent Proofs via Multi-Focusing. Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, Sep 2008, Milano, Italy. pp.383-396, ⟨10.1007/978-0-387-09680-3_26⟩. ⟨hal-00527893⟩

Chuck Liang, Dale Miller. Focusing and Polarization in Intuitionistic Logic. Computer Science Logic, Sep 2007, Lausanne, Switzerland. ⟨inria-00167231⟩

Alexis Saurin, Dale Miller. From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic. 16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Sep 2007, Lausanne, Switzerland. pp.405-419, ⟨10.1007/978-3-540-74915-8_31⟩. ⟨hal-00527888⟩

Dale Miller. Collection analysis for Horn clause programs. International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Jul 2006, Venice, Italy. ⟨inria-00167225⟩

Axelle Ziegler, Dale Miller, Catuscia Palamidessi. A Congruence Format for Name-passing Calculi. 2nd Workshop on Structural Operational Semantics (SOS'05), Jul 2005, Lisboa, Portugal. pp.169-189, ⟨10.1016/j.entcs.2005.09.032⟩. ⟨inria-00201085⟩

Alexis Saurin, Dale Miller. A game semantics for proof search, preliminary results. Twenty-first Conference on the Mathematical Foundations of Programming Semantics - MFPS XXI, May 2005, Birmingham, United Kingdom. pp.543-563, ⟨10.1016/j.entcs.2005.11.072⟩. ⟨hal-00527881⟩

Dale Miller. Influences between logic programming and proof theory. HaPoP 2018: Fourth Symposium on the History and Philosophy of Programming, Mar 2018, Oxford, United Kingdom. ⟨hal-01900891⟩

Thomas Henzinger, Dale Miller. Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). ACM, pp.1-764, 2014, 978-1-4503-2886-9. ⟨hal-01087515⟩

Gramlich Bernhard, Dale Miller, Sattler Uli. Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 2012, Proceedings. Springer, 7364, pp.1-568, 2012, Lecture Notes in Artificial Intelligence, ⟨10.1007/978-3-642-31365-3⟩. ⟨hal-00776254⟩

Hawblitzel Chris, Dale Miller. CPP 2012: Second International Conference on Certified Programs and Proofs. Springer, 7679, pp.1-305, 2012, lncs, ⟨10.1007/978-3-642-35308-6⟩. ⟨hal-00776263⟩

Dale Miller, Zoltán Ésik. Proceedings 8th Workshop on Fixed Points in Computer Science. Electronic Proceedings in Theoretical Computer Science, 77, pp.61, 2012, ⟨10.4204/EPTCS.77⟩. ⟨hal-00776273⟩

Dale Miller, Nadathur Gopalan. Programming with Higher-Order Logic. Cambridge University Press, pp.320, 2012, 9780521879408. ⟨10.1017/CBO9781139021326⟩. ⟨hal-00776197⟩

Roberto Di Cosmo, Dale Miller. Linear Logic. Edward N. Zalta. The Stanford Encyclopedia of Philosophy, The Metaphysics Research Lab Center for the Study of Language and Information Stanford University Stanford, CA 94305-4115, http://plato.stanford.edu/archives/fall2006/entries/logic-linear/, 2006. ⟨hal-00160648⟩

Dale Miller. 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Dale Miller. FSCD 2017 - 2nd International Conference on Formal Structures for Computation and Deduction , Sep 2017, Oxford, United Kingdom. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2017, 978-3-95977-047-7. ⟨hal-01615598⟩

Matteo Manighetti, Dale Miller. Computational logic based on linear logic and fixed points. 2022. ⟨hal-03579451⟩

Chuck Liang, Dale Miller. Focusing Gentzen's LK proof system. 2021. ⟨hal-03457379⟩

Zakaria Chihani, Danko Ilik, Dale Miller. Classical polarizations yield double-negation translations. 2016. ⟨hal-01354298⟩

Dale Miller. Communicating and trusting proofs: The case for foundational proof certificates. 2013. ⟨hal-00772727⟩

Dale Miller, Alwen Tiu. Extracting Proofs from Tabled Proof Search. 2013. ⟨hal-00863561⟩

Roberto Blanco, Matteo Manighetti, Dale Miller. FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs. [Research Report] Inria Saclay. 2020. ⟨hal-02974002⟩

Vivek Nigam, Dale Miller. Focusing in linear meta-logic: extended report. [Research Report] Maybe this file need a better style. Specially the proofs., 2008. ⟨inria-00281631⟩

Amy Felty, Dale Miller. Encoding a dependent-type -calculus in a logic programming language. [Research Report] RR-1259, INRIA. 1990, pp.15. ⟨inria-00075299⟩