Accéder directement au contenu

Dale Miller

80
Documents

Publications

A Survey of the Proof-Theoretic Foundations of Logic Programming

Dale Miller
Theory and Practice of Logic Programming, 2022, 22 (6), pp.859 - 904. ⟨10.1017/S1471068421000533⟩
Article dans une revue hal-03411144v1
Image document

From axioms to synthetic inference rules via focusing

Sonia Marin , Dale Miller , Elaine Pimentel , Marco Volpe
Annals of Pure and Applied Logic, 2022, 173 (5), pp.103091. ⟨10.1016/j.apal.2022.103091⟩
Article dans une revue hal-03792129v1

Functions-as-constructors higher-order unification: extended pattern unification

Tomer Libal , Dale Miller
Annals of Mathematics and Artificial Intelligence, 2021, ⟨10.1007/s10472-021-09774-y⟩
Article dans une revue hal-03457303v1
Image document

Reciprocal Influences Between Proof Theory and Logic Programming

Dale Miller
Philosophy & Technology, 2021, 34, pp.75-104. ⟨10.1007/s13347-019-00370-x⟩
Article dans une revue hal-02368867v1
Image document

The undecidability of proof search when equality is a logical connective

Dale Miller , Alexandre Viel
Annals of Mathematics and Artificial Intelligence, 2021, ⟨10.1007/s10472-021-09764-0⟩
Article dans une revue hal-03457312v1
Image document

Mechanized metatheory revisited

Dale Miller
Journal of Automated Reasoning, 2019, 63 (3), pp.625-665. ⟨10.1007/s10817-018-9483-3⟩
Article dans une revue hal-01884210v1
Image document

A proof theory for model checking

Quentin Heath , Dale Miller
Journal of Automated Reasoning, 2019, 63 (4), pp.857-885. ⟨10.1007/s10817-018-9475-3⟩
Article dans une revue hal-01814006v1
Image document

A Semantic Framework for Proof Evidence

Zakaria Chihani , Dale Miller , Fabien Renaud
Journal of Automated Reasoning, 2017, 59 (3), pp.287-330. ⟨10.1007/s10817-016-9380-6⟩
Article dans une revue hal-01390912v1
Image document

Proof Certificates for Equality Reasoning

Zakaria Chihani , Dale Miller
Electronic Notes in Theoretical Computer Science, 2016, 323, pp.93 - 108. ⟨10.1016/j.entcs.2016.06.007⟩
Article dans une revue hal-01390919v1
Image document

Preserving differential privacy under finite-precision semantics

Ivan Gazeau , Dale Miller , Catuscia Palamidessi
Theoretical Computer Science, 2016
Article dans une revue hal-01390927v1
Image document

A Multi-Focused Proof System Isomorphic to Expansion Proofs

Kaustuv Chaudhuri , Stefan Hetzl , Dale Miller
Journal of Logic and Computation, 2014
Article dans une revue hal-00937056v1
Image document

Abella: A System for Reasoning about Relational Specifications

David Baelde , Kaustuv Chaudhuri , Andrew Gacek , Dale Miller , Gopalan Nadathur
Journal of Formalized Reasoning, 2014, Special Issue: User Tutorials 2, 7 (2), pp.1-89. ⟨10.6092/issn.1972-5787/4650⟩
Article dans une revue hal-01102709v1
Image document

Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic

Chuck Liang , Dale Miller
Annals of Pure and Applied Logic, 2013, 164 (2), pp.86-111. ⟨10.1016/j.apal.2012.09.005⟩
Article dans une revue hal-00787601v1

A formal framework for specifying sequent calculus proof systems

Dale Miller , Elaine Pimentel
Theoretical Computer Science, 2013, pp.98-116. ⟨10.1016/j.tcs.2012.12.008⟩
Article dans une revue hal-00787586v1

A two-level logic approach to reasoning about computations

Andrew Gacek , Dale Miller , Gopalan Nadathur
Journal of Automated Reasoning, 2012, 49 (2), pp.241-273. ⟨10.1007/s10817-011-9218-1⟩
Article dans une revue hal-00776208v1
Image document

A Focused Approach to Combining Logics

Chuck Liang , Dale Miller
Annals of Pure and Applied Logic, 2011, ⟨10.1016/j.apal.2011.01.012⟩
Article dans une revue hal-00772736v1
Image document

Nominal Abstraction

Gacek Andrew , Dale Miller , Gopalan Nadathur
Information and Computation, 2011, 209 (1), pp.48-73
Article dans une revue hal-00772606v1

Proof and Refutation in MALL as a game

Olivier Delande , Dale Miller , Alexis Saurin
Annals of Pure and Applied Logic, 2010, 161 (5), pp.654-672. ⟨10.1016/j.apal.2009.07.017⟩
Article dans une revue hal-00527922v1
Image document

Proof Search Specifications of the pi-calculus

Tiu Alwen , Dale Miller
ACM Transactions on Computational Logic, 2010, 11 (2)
Article dans une revue hal-00772571v1
Image document

A framework for proof systems

Nigam Vivek , Dale Miller
Journal of Automated Reasoning, 2010, 45 (2)
Article dans une revue hal-00772562v1

Focusing and Polarization in Linear, Intuitionistic, and Classical Logics

Chuck Liang , Dale Miller
Theoretical Computer Science, 2009, 410 (46), ⟨10.1016/j.tcs.2009.07.041⟩
Article dans une revue hal-00772342v1
Image document

Formal Reasoning using Distributed Assertions

Farah Al Wardani , Kaustuv Chaudhuri , Dale Miller
FroCoS 2023 - 14th International Symposium on Frontiers of Combining Systems, Sep 2023, Prague (Czech Republic), Czech Republic
Communication dans un congrès hal-04167922v2
Image document

A positive perspective on term representation: Extended paper

Dale Miller , Jui-Hsuan Wu
CSL 2023 - Computer Science Logic, Feb 2023, Warsaw, Poland
Communication dans un congrès hal-03843587v2
Image document

A system of inference based on proof search: an extended abstract

Dale Miller
LICS 2023 - 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2023, Boston, United States. pp.1-11, ⟨10.1109/LICS56636.2023.10175827⟩
Communication dans un congrès hal-04169014v2

Two Applications of Logic Programming to Coq

Matteo Manighetti , Dale Miller , Alberto Momigliano
26th International Conference on Types for Proofs and Programs (TYPES 2020), Mar 2020, Turin, Italy
Communication dans un congrès hal-03457352v1
Image document

A Distributed and Trusted Web of Formal Proofs

Dale Miller
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⟩
Communication dans un congrès hal-02468229v1
Image document

Functional programming with $λ$-tree syntax

Ulysse Gérard , Dale Miller , Gabriel Scherer
PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-16, ⟨10.1145/3354166.3354177⟩
Communication dans un congrès hal-02368906v1
Image document

Property-Based Testing via Proof Reconstruction

Roberto Blanco , Dale Miller , Alberto Momigliano
PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-13, ⟨10.1145/3354166.3354170⟩
Communication dans un congrès hal-02368931v1
Image document

A Proof-Theoretic Approach to Certifying Skolemization

Kaustuv Chaudhuri , Matteo Manighetti , Dale Miller
CPP 2019 - 8th ACM SIGPLAN International Conference, Jan 2019, Cascais, Portugal. pp.78-90, ⟨10.1145/3293880.3294094⟩
Communication dans un congrès hal-02368946v1
Image document

Functional programming with λ$-tree$ syntax: a progress report

Ulysse Gérard , Dale Miller
13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2018, Oxford, United Kingdom
Communication dans un congrès hal-01806129v2
Image document

Computation-as-deduction in Abella: work in progress

Kaustuv Chaudhuri , Ulysse Gérard , Dale Miller
13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2018, Oxford, United Kingdom
Communication dans un congrès hal-01806154v1
Image document

Using linear logic and proof theory to unify computational logic

Dale Miller
Proceedings of Trends in Linear Logic and Applications (TLLA 17), Sep 2017, Oxford, United Kingdom
Communication dans un congrès hal-01615673v1
Image document

Property-Based Testing via Proof Reconstruction Work-in-progress

Roberto Blanco , Dale Miller , Alberto Momigliano
LFMTP 17: Logical Frameworks and Meta-Languages: Theory and Practice, Sep 2017, Oxford, United Kingdom
Communication dans un congrès hal-01646788v1
Image document

Separating Functional Computation from Relations

Ulysse Gérard , Dale Miller
26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. pp.23:1--23:17
Communication dans un congrès hal-01615683v1
Image document

Translating Between Implicit and Explicit Versions of Proof

Roberto Blanco , Zakaria Chihani , Dale Miller
CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden
Communication dans un congrès hal-01645016v1
Image document

Mechanized Metatheory Revisited: An Extended Abstract

Dale Miller
Post-proceedings of TYPES 2016 , 2017, Novi Sad, Serbia. ⟨10.4230/LIPIcs⟩
Communication dans un congrès hal-01615681v1

Linear logic as a logical framework

Dale Miller
Proceedings of Structures and Deduction (SD) 2017, Sep 2017, Oxford, United Kingdom
Communication dans un congrès hal-01615664v1
Image document

Functions-as-constructors Higher-order Unification

Tomer Libal , Dale Miller
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⟩
Communication dans un congrès hal-01379683v1
Image document

A focused framework for emulating modal proof systems

Sonia Marin , Dale Miller , Marco Volpe
11th conference on "Advances in Modal Logic", Aug 2016, Budapest, Hungary. pp.469-488
Communication dans un congrès hal-01379624v1
Image document

Defining the meaning of TPTP formatted proofs

Roberto Blanco , Tomer Libal , Dale Miller
11th International Workshop on the Implementation of Logics, Nov 2015, Suva, Fiji
Communication dans un congrès hal-01238434v1
Image document

On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control

Chuck Liang , Dale Miller
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⟩
Communication dans un congrès hal-01239753v1
Image document

Focused labeled proof systems for modal logic

Dale Miller , Marco Volpe
20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji
Communication dans un congrès hal-01213858v1
Image document

A framework for proof certificates in finite state exploration

Quentin Heath , Dale Miller
Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, Aug 2015, Berlin, Germany. ⟨10.4204/EPTCS.186.4⟩
Communication dans un congrès hal-01240172v1
Image document

A Lightweight Formalization of the Metatheory of Bisimulation-Up-To

Kaustuv Chaudhuri , Matteo Cimini , Dale Miller
4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP), ACM-SIGPLAN, Jan 2015, Mumbai, India. ⟨10.1145/2676724.2693170⟩
Communication dans un congrès hal-01091524v1
Image document

Proof Outlines as Proof Certificates: A System Description

Roberto Blanco , Dale Miller
First International Workshop on Focusing, Nov 2015, Suva, Fiji
Communication dans un congrès hal-01238436v1
Image document

Foundational proof certificates in first-order logic

Zakaria Chihani , Dale Miller , Fabien Renaud
CADE - 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, United States
Communication dans un congrès hal-00906485v1
Image document

Unifying Classical and Intuitionistic Logics for Computational Control

Chuck Liang , Dale Miller
LOGIC IN COMPUTER SCIENCE (LICS 2013), Jun 2013, New Orleans, United States
Communication dans un congrès hal-00906299v1
Image document

Checking foundational proof certificates for first-order logic

Zakaria Chihani , Dale Miller , Fabien Renaud
PxTP - Proof Exchange for Theorem Proving, Jun 2013, Lake Placid, United States
Communication dans un congrès hal-00906486v1
Image document

Preserving differential privacy under finite-precision semantics

Ivan Gazeau , Dale Miller , Catuscia Palamidessi
QAPL - 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, Mar 2013, Rome, Italy. pp.1-18, ⟨10.4204/EPTCS.117.1⟩
Communication dans un congrès hal-00780774v2
Image document

A non-local method for robustness analysis of floating point programs

Ivan Gazeau , Dale Miller , Catuscia Palamidessi
QAPL - Tenth Workshop on Quantitative Aspects of Programming Languages, Mar 2012, Tallinn, Estonia. pp.63-76, ⟨10.4204/EPTCS.85.5⟩
Communication dans un congrès hal-00665995v3
Image document

A Systematic Approach to Canonicity in the Classical Sequent Calculus

Kaustuv Chaudhuri , Stefan Hetzl , Dale Miller
21st EACSL Annual Conference on Computer Science Logic, Sep 2012, Fontainebleau, France. pp.183-197, ⟨10.4230/LIPIcs.CSL.2012.183⟩
Communication dans un congrès hal-00772396v1
Image document

A proposal for broad spectrum proof certificates

Dale Miller
CPP 2011 - First International Conference on Certified Proofs and Programs, 2011, Kenting, Taiwan
Communication dans un congrès hal-00772722v1
Image document

FICS 2010

Dale Miller , Arnaud Carayol , Panos Rondogiannis , Lars Birkedal , Marek Czarnecki
7th Workshop on Fixed Points in Computer Science, FICS 2010, Aug 2010, Brno, Czech Republic. pp.89
Communication dans un congrès hal-00512377v1
Image document

Reasoning about computations using two-levels of logic

Dale Miller
APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems, 2010, Shanghai, China
Communication dans un congrès hal-00772599v1
Image document

Finding Unity in Computational Logic

Dale Miller
ACM-BCS Visions of Computer Science, 2010, Edinburgh, United Kingdom
Communication dans un congrès hal-00772557v1
Image document

Focused Inductive Theorem Proving

David Baelde , Dale Miller , Zachary Snow
IJCAR 2010 - International Joint Conference on Automated Deduction, 2010, Edinburgh, United Kingdom
Communication dans un congrès hal-00772592v1

Algorithmic specifications in linear logic with subexponentials

Nigam Vivek , Dale Miller
PPDP09 - ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Sep 2009, Coimbra, Portugal
Communication dans un congrès hal-00772332v1

A Unified Sequent Calculus for Focused Proofs

Liang Chuck , Dale Miller
LICS 2009 - Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE, Aug 2009, Los Angeles, United States
Communication dans un congrès hal-00772347v1

Canonical Sequent Proofs via Multi-Focusing

Alexis Saurin , Kaustuv C. Chaudhuri , Dale Miller
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⟩
Communication dans un congrès hal-00527893v1
Image document

Focusing and Polarization in Intuitionistic Logic

Chuck Liang , Dale Miller
Computer Science Logic, Sep 2007, Lausanne, Switzerland
Communication dans un congrès inria-00167231v1

From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic

Alexis Saurin , Dale Miller
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⟩
Communication dans un congrès hal-00527888v1
Image document

Collection analysis for Horn clause programs

Dale Miller
International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Jul 2006, Venice, Italy
Communication dans un congrès inria-00167225v1
Image document

A Congruence Format for Name-passing Calculi

Axelle Ziegler , Dale Miller , Catuscia Palamidessi
2nd Workshop on Structural Operational Semantics (SOS'05), Jul 2005, Lisboa, Portugal. pp.169-189, ⟨10.1016/j.entcs.2005.09.032⟩
Communication dans un congrès inria-00201085v1

A game semantics for proof search, preliminary results

Alexis Saurin , Dale Miller
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⟩
Communication dans un congrès hal-00527881v1
Image document

Influences between logic programming and proof theory

Dale Miller
HaPoP 2018: Fourth Symposium on the History and Philosophy of Programming, Mar 2018, Oxford, United Kingdom
Document associé à des manifestations scientifiques hal-01900891v1

Linear Logic

Roberto Di Cosmo , Dale Miller
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
Chapitre d'ouvrage hal-00160648v1