Dale Miller. Mechanized metatheory revisited. Journal of Automated Reasoning, Springer Verlag, In press. 〈hal-01884210〉

Quentin Heath, Dale Miller. A proof theory for model checking. Journal of Automated Reasoning, Springer Verlag, In press, 〈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〉

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〉

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〉

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〉

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〉

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. Journal of 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〉

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

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〉

Liang Chuck, 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〉

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. 2018. 〈hal-01806154〉

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〉

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

Ulysse Gérard, Dale Miller. Separating Functional Computation from Relations. 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. 82 (23), pp.23:1--23:17, 2017, LIPIcs. 〈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. 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〉

Sonia Marin, Dale Miller, Marco Volpe. A focused framework for emulating modal proof systems. Lev Beklemishev; Stéphane Demri; András Máté. 11th conference on "Advances in Modal Logic", Aug 2016, Budapest, Hungary. College Publications, pp.469-488, Advances in Modal Logic. 〈hal-01379624〉

Tomer Libal, Dale Miller. Functions-as-constructors Higher-order Unification. 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Jun 2016, Porto, Portugal. Leibniz International Proceedings in Informatics (LIPIcs), pp.1 - 17, 2016, 〈10.4230/LIPIcs.FSCD.2016.26〉. 〈hal-01379683〉

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. 2015, 〈10.4204/EPTCS.186.4〉. 〈hal-01240172〉

Chuck Liang, Dale Miller. On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control. Martin Davis; Ansgar Fehnker; Annabelle McIver; Andrei Voronkov. LPAR 20 - International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. Springer, 9450, pp.297-312, 2015, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-662-48899-7_21〉. 〈hal-01239753〉

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. 〈http://www.eprover.org/EVENTS/IWIL-2015.html〉. 〈hal-01238434〉

Roberto Blanco, Dale Miller. Proof Outlines as Proof Certificates: A System Description. First International Workshop on Focusing, Nov 2015, Suva, Fiji. 〈http://www.qatar.cmu.edu/iliano/svc/conf/wof15/〉. 〈hal-01238436〉

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〉

Kaustuv Chaudhuri, Matteo Cimini, Dale Miller. A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. Xavier Leroy and Alwen Tiu. 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP), Jan 2015, Mumbai, India. ACM Proceedings, 2014, 〈http://cpp2015.inria.fr〉. 〈10.1145/2676724.2693170〉. 〈hal-01091524〉

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

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. 2013. 〈hal-00906485〉

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. 2013. 〈hal-00906486〉

Ivan Gazeau, Dale Miller, Catuscia Palamidessi. Preserving differential privacy under finite-precision semantics. Luca Bortolussi and Herbert Wiklicky. QAPL - 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, Mar 2013, Rome, Italy. Open Publishing Association, 117, pp.1-18, 2013, Electronic Proceedings in Theoretical Computer Science. 〈10.4204/EPTCS.117.1〉. 〈hal-00780774v2〉

Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. Patrick Cégielski and Arnaud Durand. 21st EACSL Annual Conference on Computer Science Logic, Sep 2012, Fontainebleau, France. 16, pp.183-197, 2012, Leibniz International Proceedings in Informatics (LIPIcs). 〈10.4230/LIPIcs.CSL.2012.183〉. 〈hal-00772396〉

Ivan Gazeau, Dale Miller, Catuscia Palamidessi. A non-local method for robustness analysis of floating point programs. Mieke Massink and Herbert Wiklicky. QAPL - Tenth Workshop on Quantitative Aspects of Programming Languages, Mar 2012, Tallinn, Estonia. Open Publishing Association, 8555, pp.63-76, 2012, EPTCS. 〈10.4204/EPTCS.85.5〉. 〈hal-00665995v3〉

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

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

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

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

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

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. 2009. 〈hal-00772347〉

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. 2009. 〈hal-00772332〉

Alexis Saurin, Kaustuv 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, 2008, 〈10.1007/978-0-387-09680-3_26〉. 〈hal-00527893〉

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. Springer, pp.405-419, 2007, Lecture notes in computer science. 〈10.1007/978-3-540-74915-8_31〉. 〈hal-00527888〉

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

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〉

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. 155, pp.543-563, 2006, 〈10.1016/j.entcs.2005.11.072〉. 〈hal-00527881〉

Axelle Ziegler, Dale Miller, Catuscia Palamidessi. A Congruence Format for Name-passing Calculi. Peter Mosses and Irek Ulidowski. 2nd Workshop on Structural Operational Semantics (SOS'05), Jul 2005, Lisboa, Portugal. Elsevier, 156 (1), pp.169-189, 2006, Electronic Notes in Theoretical Computer Science. 〈10.1016/j.entcs.2005.09.032〉. 〈inria-00201085〉

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. 〈http://dl.acm.org/citation.cfm?id=2603088〉. 〈hal-01087515〉

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〉

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〉

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〉

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

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

Dale Miller. Communicating and trusting proofs: The case for foundational proof certificates. To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science.. 2013. 〈hal-00772727〉

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〉