Skip to Main content
Number of documents

70


Journal articles17 documents

Conference papers39 documents

  • 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⟩
  • 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, 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⟩
  • 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⟩
  • 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⟩
  • Dale Miller. Mechanized Metatheory Revisited: An Extended Abstract . Post-proceedings of TYPES 2016 , 2017, Novi Sad, Serbia. ⟨10.4230/LIPIcs⟩. ⟨hal-01615681⟩
  • 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⟩
  • 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, 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⟩
  • 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⟩
  • 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⟩
  • 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⟩
  • 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⟩
  • Roberto Blanco, Dale Miller. Proof Outlines as Proof Certificates: A System Description. First International Workshop on Focusing, Nov 2015, Suva, Fiji. ⟨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⟩
  • 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. 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⟩
  • 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⟩
  • 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⟩
  • 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⟩
  • 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⟩
  • 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. 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⟩
  • 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⟩
  • 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⟩
  • 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⟩
  • 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, ⟨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⟩

Documents associated with scientific events1 document

  • 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⟩

Books5 documents

  • 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⟩
  • 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⟩
  • 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, Nadathur Gopalan. Programming with Higher-Order Logic. Cambridge University Press, pp.320, 2012, 9780521879408. ⟨10.1017/CBO9781139021326⟩. ⟨hal-00776197⟩

Book sections1 document

  • 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⟩

Directions of work or proceedings1 document

  • 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⟩

Preprints, Working Papers, ...3 documents

  • 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⟩

Reports3 documents

  • 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⟩