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. Journal of Theoretical Computer Science (TCS), Elsevier, 2016. <hal-01390927>

Zakaria Chihani, Dale Miller, Fabien Renaud. A Semantic Framework for Proof Evidence. Journal of Automated Reasoning, Springer Verlag, 2016, <10.1007/s10817-016-9380-6>. <hal-01390912>

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>

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

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>

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>

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>

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>

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>

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>

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>

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>

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>

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>

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>

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>

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. 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; Proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL). <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>

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>

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>

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>

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; Proceedings of the 2nd Workshop on Structural Operational Semantics. <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. 155, pp.543-563, 2006, <10.1016/j.entcs.2005.11.072>. <hal-00527881>

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.305, 2012, lncs, <10.1007/978-3-642-35308-6>. <hal-00776263>

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

Gramlich Bernhard, Dale Miller, Sattler Uli. Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 2012, Proceedings. Springer, 7364, pp.568, 2012, lnai, <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>

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>

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. To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science.. 2013. <hal-00772727>

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

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>