@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -ob miller.bib -c 'author : "\(Dale\|Dale A.\) Miller"' master.bib}}
@preamble{{\newcommand{\Plato}[1]{}}}
@article{andrews84ahol,
author = {Peter B. Andrews and Eve Longini-Cohen and Dale Miller
and Frank Pfenning},
journal = {Contemp. Math},
pages = {169--192},
title = {Automating Higher Order Logics},
volume = {29},
year = {1984}
}
@incollection{andrews84ams,
title = {Automating higher order logic},
author = {Peter B. Andrews and Eve Longini Cohen and Dale Miller
and Frank Pfenning},
booktitle = {Automated Theorem Proving: After 25 Years},
editor = {W. W. Bledsoe and D. W. Loveland},
publisher = {American Mathematical Society},
address = {Providence, RI},
year = {1984},
pages = {169--192}
}
@manual{baelde06manual,
title = {A User Guide to {Bedwyr}},
author = {David Baelde and Andrew Gacek and Dale Miller and
Gopalan Nadathur and Alwen Tiu},
month = nov,
pdf = {https://gforge.inria.fr/docman/view.php/367/705/userguide.pdf},
year = {2006}
}
@inproceedings{baelde07cade,
author = {David Baelde and Andrew Gacek and Dale Miller and
Gopalan Nadathur and Alwen Tiu},
title = {The {Bedwyr} system for model checking over syntactic
expressions},
booktitle = {21th Conf.\ on Automated Deduction (CADE)},
pages = {391--397},
year = {2007},
editor = {F. Pfenning},
number = {4603},
series = {LNAI},
publisher = {Springer},
address = {New York},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/cade2007.pdf},
doi = {10.1007/978-3-540-73595-3_28}
}
@inproceedings{baelde07lpar,
author = {David Baelde and Dale Miller},
title = {Least and greatest fixed points in linear logic},
booktitle = {International Conference on Logic for Programming and
Automated Reasoning (LPAR)},
editor = {N. Dershowitz and A. Voronkov},
pages = {92--106},
series = {LNCS},
volume = {4790},
year = {2007},
doi = {10.1007/978-3-540-75560-9\_9}
}
@unpublished{baelde07tr,
author = {David Baelde and Dale Miller},
title = {Least and greatest fixed points in linear logic:
extended version},
note = {Technical report, available from the first author's
web page},
month = apr,
year = {2007},
url = {https://www.lix.polytechnique.fr/~dbaelde/productions/pool/mumall_draft_long.pdf}
}
@inproceedings{baelde10ijcar,
author = {David Baelde and Dale Miller and Zachary Snow},
title = {Focused Inductive Theorem Proving},
booktitle = {Fifth International Joint Conference on Automated
Reasoning},
year = {2010},
pages = {278--292},
editor = {J. Giesl and R. H{\"a}hnle},
series = {LNCS},
number = {6173},
doi = {10.1007/978-3-642-14203-1\_24}
}
@article{baelde14jfr,
author = {David Baelde and Kaustuv Chaudhuri and Andrew Gacek
and Dale Miller and Gopalan Nadathur and Alwen Tiu and
Yuting Wang},
title = {Abella: {A} System for Reasoning about Relational
Specifications},
journal = {J. of Formalized Reasoning},
year = {2014},
volume = {7},
number = {2},
pages = {1--89},
doi = {10.6092/issn.1972-5787/4650}
}
@incollection{benzmueller14lc,
author = {Christoph Benzm{\"u}ller and Dale Miller},
title = {Automation of Higher-Order Logic},
booktitle = {Computational Logic},
publisher = {North Holland},
year = {2014},
editor = {J. Siekmann},
volume = {9},
pages = {215--254},
series = {Handbook of the History of Logic},
isbn = {978-0-444-51624-4},
doi = {10.1016/B978-0-444-51624-4.50005-8}
}
@inproceedings{blanco15iwil,
author = {Roberto Blanco and Tomer Libal and Dale Miller},
title = {Defining the meaning of {TPTP} formatted proofs},
url = {https://www.eprover.org/EVENTS/IWIL-2015.html},
booktitle = {IWIL-2015. 11th International Workshop on the
Implementation of Logics},
editor = {Boris Konev and Stephan Schulz and Laurent Simon},
series = {EPiC Series in Computing},
volume = {40},
pages = {78--90},
year = {2016},
publisher = {EasyChair}
}
@inproceedings{blanco15wof,
author = {Roberto Blanco and Dale Miller},
title = {Proof Outlines as Proof Certificates: a system
description},
year = {2015},
url = {https://www.eprover.org/EVENTS/IWIL-2015.html},
month = nov,
editor = {Iliano Cervesato and Carsten Sch{\"u}rmann},
booktitle = {Proceedings First International Workshop on Focusing},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {197},
publisher = {Open Publishing Association},
pages = {7--14},
doi = {10.4204/EPTCS.197.2}
}
@inproceedings{blanco17cade,
author = {Roberto Blanco and Zakaria Chihani and Dale Miller},
title = {Translating Between Implicit and Explicit Versions of
Proof},
booktitle = {Automated Deduction - {CADE} 26 - 26th International
Conference on Automated Deduction, Gothenburg, Sweden,
August 6-11, 2017, Proceedings},
pages = {255--273},
year = {2017},
doi = {10.1007/978-3-319-63046-5\_16},
editor = {Leonardo de Moura},
series = {LNCS},
volume = {10395},
publisher = {Springer}
}
@inproceedings{blanco17lfmtp,
author = {Roberto Blanco and Dale Miller and Alberto
Momigliano},
title = {Property-Based Testing via Proof Reconstruction},
booktitle = {Work-in-Progress Proceedings of the Workshop on
Logical Frameworks and Meta-Languages: Theory and
Practice},
pages = {17--22},
year = {2017},
url = {https://www.dimi.uniud.it/la-ricerca/pubblicazioni/preprints/5.2017/},
editor = {Marino Miculan and Florian Rabe},
series = {Technical reports of DIMI, University of Udine}
}
@inproceedings{blanco19ppdp,
author = {Roberto Blanco and Dale Miller and Alberto
Momigliano},
title = {Property-Based Testing via Proof Reconstruction},
booktitle = {Principles and Practice of Programming Languages 2019
(PPDP '19)},
year = {2019},
editor = {E. Komendantskaya},
month = oct,
doi = {10.1145/3354166.3354170}
}
@techreport{blanco20coq,
author = {Roberto Blanco and Matteo Manighetti and Dale Miller},
title = {{FPC}-Coq: Using {ELPI} to elaborate external proof
evidence into Coq proofs},
institution = {Inria},
year = {2020},
number = {hal-02974002},
url = {https://hal.inria.fr/hal-02974002},
month = jul,
note = {Presented at the Coq Workshop 2020}
}
@inproceedings{chaudhuri08tcs,
author = {Kaustuv Chaudhuri and Dale Miller and Alexis Saurin},
title = {Canonical Sequent Proofs via Multi-Focusing},
booktitle = {Fifth International Conference on Theoretical Computer
Science},
publisher = {Springer},
year = {2008},
volume = {273},
series = {IFIP},
editor = {G. Ausiello and J. Karhum{\"a}ki and G. Mauri and L.
Ong},
month = sep,
pages = {383--396},
doi = {10.1007/978-0-387-09680-3\_26}
}
@inproceedings{chaudhuri12csl,
author = {Kaustuv Chaudhuri and Stefan Hetzl and Dale Miller},
title = {A Systematic Approach to Canonicity in the Classical
Sequent Calculus},
booktitle = {CSL 2012: Computer Science Logic},
year = {2012},
month = sep,
pages = {183--197},
editor = {Patrick C{\'e}gielski and Arnaud Durand},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
volume = {16},
doi = {10.4230/LIPIcs.CSL.2012.183},
isbn = {978-3-939897-42-2},
issn = {1868-8969}
}
@inproceedings{chaudhuri15cpp,
author = {Kaustuv Chaudhuri and Matteo Cimini and Dale Miller},
title = {A Lightweight Formalization of the Metatheory of
Bisimulation-Up-To},
booktitle = {Proceedings of the 4th ACM-SIGPLAN Conference on
Certified Programs and Proofs},
doi = {10.1145/2676724.2693170},
year = {2015},
editor = {Xavier Leroy and Alwen Tiu},
pages = {157--166},
month = jan,
address = {Mumbai, India},
publisher = {ACM},
url = {https://hal.inria.fr/hal-01091524/document}
}
@article{chaudhuri16jlc,
author = {Kaustuv Chaudhuri and Stefan Hetzl and Dale Miller},
title = {A Multi-Focused Proof System Isomorphic to Expansion
Proofs},
journal = {J. of Logic and Computation},
publisher = {Oxford University Press},
year = {2016},
volume = {26},
number = {2},
pages = {577--603},
doi = {10.1093/logcom/exu030}
}
@inproceedings{chihani13cade,
author = {Zakaria Chihani and Dale Miller and Fabien Renaud},
title = {Foundational proof certificates in first-order logic},
booktitle = {CADE 24: Conference on Automated Deduction 2013},
year = {2013},
editor = {Maria Paola Bonacina},
series = {LNAI},
number = {7898},
pages = {162--177},
doi = {10.1007/978-3-642-38574-2\_11}
}
@inproceedings{chihani13pxtp,
author = {Zakaria Chihani and Dale Miller and Fabien Renaud},
title = {Checking Foundational Proof Certificates for
First-Order Logic (extended abstract)},
booktitle = {Third International Workshop on Proof Exchange for
Theorem Proving (PxTP 2013)},
pages = {58--66},
year = {2013},
editor = {J. C. Blanchette and J. Urban},
volume = {14},
series = {EPiC Series},
publisher = {EasyChair}
}
@inproceedings{chihani16lfsa,
title = {Proof Certificates for Equality Reasoning},
author = {Zakaria Chihani and Dale Miller},
booktitle = {Post-proceedings of LSFA 2015: 10th Workshop on
Logical and Semantic Frameworks, with Applications.
Natal, Brazil.},
editor = {Mario Benevides and Ren\'e Thiemann},
publisher = {Elsevier},
series = {ENTCS},
number = {323},
year = {2016},
pages = {93--108},
doi = {10.1016/j.entcs.2016.06.007}
}
@misc{chihani16lprolog,
author = {Zakaria Chihani and Dale Miller and Fabien Renaud},
title = {Supporting $\lambda${Prolog} code},
note = {\url{https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fpc-support.tar}},
month = apr,
year = {2016}
}
@techreport{chihani16tr,
title = {{Classical polarizations yield double-negation
translations}},
author = {Zakaria Chihani and Danko Ilik and Dale Miller},
url = {https://hal.inria.fr/hal-01354298},
institution = {Inria Saclay},
year = {2016},
month = aug,
pdf = {https://hal.inria.fr/hal-01354298/file/main.pdf},
hal_id = {hal-01354298},
hal_version = {v1}
}
@article{chihani17jar,
author = {Zakaria Chihani and Dale Miller and Fabien Renaud},
title = {A semantic framework for proof evidence},
journal = {J. of Automated Reasoning},
year = {2017},
pages = {287--330},
volume = {59},
number = {3},
doi = {10.1007/s10817-016-9380-6}
}
@inproceedings{cimini20sle,
author = {Matteo Cimini and Dale Miller and Jeremy G. Siek},
title = {Extrinsically Typed Operational Semantics for
Functional Languages},
booktitle = {ACM SIGPLAN International Conference on Software
Language Engineering (SLE)},
year = {2020},
pages = {108--125},
editor = {Laurence Tratt and Juan de Lara},
doi = {10.1145/3426425.3426936},
month = nov,
organization = {ACM SIGPLAN},
publisher = {ACM}
}
@inproceedings{delande08lics,
author = {Olivier Delande and Dale Miller},
title = {A neutral approach to proof and refutation in {MALL}},
booktitle = {23th Symp.\ on Logic in Computer Science},
year = {2008},
editor = {F. Pfenning},
publisher = {IEEE Computer Society Press},
doi = {10.1016/j.apal.2009.07.017},
pages = {498--508}
}
@unpublished{delande08tr,
author = {Olivier Delande and Dale Miller},
title = {A neutral approach to proof and refutation in {MALL}:
extended report},
note = {Available via the authors web pages},
year = {2008}
}
@article{delande10apal,
author = {Olivier Delande and Dale Miller and Alexis Saurin},
title = {Proof and refutation in {MALL} as a game},
journal = {Annals of Pure and Applied Logic},
month = feb,
year = {2010},
pages = {654--672},
volume = {161},
number = {5},
doi = {10.1016/j.apal.2009.07.017},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/apal-games.pdf}
}
@incollection{dicosmo06sep,
author = {Roberto {Di Cosmo} and Dale Miller},
title = {Linear Logic},
booktitle = {The Stanford Encyclopedia of Philosophy},
publisher = {Stanford University},
editor = {Edward N. Zalta},
url = {https://plato.stanford.edu/archives/fall2006/entries/logic-linear/},
year = {2006}
}
@incollection{dicosmo19sep,
author = {Roberto {Di Cosmo} and Dale Miller},
title = {Linear Logic},
booktitle = {The Stanford Encyclopedia of Philosophy},
editor = {Edward N. Zalta},
howpublished = {\url{https://plato.stanford.edu/archives/sum2019/entries/logic-linear/}},
year = {2019},
edition = {Summer 2019},
publisher = {Metaphysics Research Lab, Stanford University}
}
@unpublished{felty87,
author = {Amy Felty and Dale Miller},
title = {Proof Explanation and Revision},
year = {1987},
note = {Draft}
}
@inproceedings{felty88cade,
author = {Amy Felty and Dale Miller},
title = {Specifying theorem provers in a higher-order logic
programming language},
editor = {Ewing Lusk and Ross Overbeck},
booktitle = {{Ninth International Conference on Automated
Deduction}},
address = {Argonne, IL},
publisher = {Springer},
pages = {61--80},
month = may,
year = {1988},
series = {LNCS},
number = {310},
doi = {10.1007/BFb0012823}
}
@unpublished{felty89wlpl,
author = {Amy Felty and Dale Miller},
title = {A Meta Language for Type Checking and Inference: An
Extended Abstract},
year = {1989},
note = {Presented at the 1989 Workshop on Programming Logic,
{B\aa lstad}, Sweden}
}
@inproceedings{felty90cade,
author = {Amy Felty and Dale Miller},
title = {Encoding a Dependent-Type $\lambda$-Calculus in a
Logic Programming Language},
booktitle = {Proceedings of the 1990 Conference on Automated
Deduction},
publisher = {Springer},
series = {LNAI},
volume = {449},
pages = {221--235},
editor = {Mark Stickel},
year = {1990}
}
@inproceedings{gacek08lfmtp,
author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
title = {Reasoning in {A}bella about Structural Operational
Semantics Specifications},
booktitle = {International Workshop on Logical Frameworks and
Meta-Languages: Theory and Practice (LFMTP 2008)},
year = {2008},
editor = {A. Abel and C. Urban},
series = {ENTCS},
number = {228},
pages = {85--100},
pdf = {https://arxiv.org/pdf/0804.3914.pdf},
doi = {10.1016/j.entcs.2008.12.118}
}
@inproceedings{gacek08lics,
author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
title = {Combining generic judgments with recursive
definitions},
booktitle = {23th Symp.\ on Logic in Computer Science},
year = {2008},
editor = {F. Pfenning},
publisher = {IEEE Computer Society Press},
pages = {33--44},
doi = {10.1109/LICS.2008.33},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics08a.pdf}
}
@techreport{gacek09corr,
author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
title = {Nominal abstraction},
note = {Extended version LICS 2008 paper. Submitted},
month = aug,
year = {2009},
pdf = {https://arxiv.org/abs/0908.1390},
institution = {CoRR}
}
@article{gacek11ic,
author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
title = {Nominal abstraction},
journal = {Information and Computation},
year = {2011},
volume = {209},
number = {1},
pages = {48--73},
doi = {10.1016/j.ic.2010.09.004},
pdf = {https://arxiv.org/abs/0908.1390}
}
@article{gacek12jar,
author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
title = {A two-level logic approach to reasoning about
computations},
year = {2012},
url = {https://arxiv.org/abs/0911.2993},
doi = {10.1007/s10817-011-9218-1},
journal = {J. of Automated Reasoning},
volume = {49},
number = {2},
pages = {241--273}
}
@unpublished{gazeau.rewriting,
author = {Ivan Gazeau and Dale Miller and Catuscia Palamidessi},
title = {Non-local robustness analysis via rewriting
techniques},
month = sep,
year = {2012},
note = {An earlier version of this paper appeared in the
pre-proceedings of QFM 2012.},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/qapl-full-version.pdf}
}
@techreport{gazeau12hal,
hal_id = {hal-00665995},
institution = {INRIA},
url = {https://hal.inria.fr/hal-00665995},
title = {{A non-local method for robustness analysis of
floating point programs}},
author = {Ivan Gazeau and Dale Miller and Catuscia Palamidessi},
booktitle = {{QAPL - Tenth Workshop on Quantitative Aspects of
Programming Languages}},
address = {Tallinn, Estonie},
year = {2012},
month = feb,
note = {To appear in QAPL 2012.},
pdf = {https://hal.inria.fr/hal-00665995/PDF/proof\_example.pdf}
}
@inproceedings{gazeau12qapl,
author = {Ivan Gazeau and Dale Miller and Catuscia Palamidessi},
title = {A non-local method for robustness analysis of floating
point programs},
booktitle = {Proceedings of the 10th Workshop on Quantitative
Aspects of Programming Languages and Systems (QAPL
2012)},
pages = {63--76},
year = {2012},
editor = {Herbert Wiklicky and Mieke Massink},
volume = {85},
series = {Electronic Proceedings in Theoretical Computer
Science},
doi = {10.4204/EPTCS.85.5}
}
@inproceedings{gazeau13qapl,
author = {Ivan Gazeau and Dale Miller and Catuscia Palamidessi},
title = {Preserving differential privacy under finite-precision
semantics},
booktitle = {Proceedings 11th International Workshop on
Quantitative Aspects of Programming Languages and
Systems (QAPL)},
url = {https://hal.inria.fr/hal-00780774},
year = {2013},
pages = {1--18}
}
@article{gazeau16tcs,
author = {Ivan Gazeau and Dale Miller and Catuscia Palamidessi},
title = {Preserving differential privacy under finite-precision
semantics},
journal = {Theoretical Computer Science},
year = {2016},
doi = {10.1016/j.tcs.2016.01.015},
pages = {92--108},
volume = {655}
}
@unpublished{gerard.mlts,
author = {Ulysse G\'erard and Dale Miller},
title = {Functional programming with $\lambda$-tree syntax:
Draft},
note = {Available from \url{https://trymlts.github.io/}.},
month = may,
year = {2018}
}
@inproceedings{gerard17csl,
author = {Ulysse G\'erard and Dale Miller},
title = {Separating Functional Computation from Relations},
booktitle = {26th EACSL Annual Conference on Computer Science Logic
(CSL 2017)},
year = {2017},
editor = {Valentin Goranko and Mads Dam},
volume = {82},
series = {LIPIcs},
pages = {23:1--23:17},
doi = {10.4230/LIPIcs.CSL.2017.23}
}
@inproceedings{gerard18lfmtp,
title = {{Functional programming with $\lambda$-tree syntax: a
progress report}},
author = {Ulysse G{\'e}rard and Dale Miller},
url = {https://hal.inria.fr/LFMTP-2018/hal-01806129v1},
booktitle = {{13th international Workshop on Logical Frameworks and
Meta-Languages: Theory and Practice}},
address = {Oxford, United Kingdom},
year = {2018},
month = jul,
pdf = {https://hal.inria.fr/hal-01806129/file/paper.pdf}
}
@inproceedings{gerard19ppdp,
author = {Ulysse G{\'e}rard and Dale Miller and Gabriel
Scherer},
title = {Functional programming with $\lambda$-tree syntax},
booktitle = {Principles and Practice of Programming Languages 2019
(PPDP '19)},
year = {2019},
editor = {E. Komendantskaya},
doi = {10.1145/3354166.3354177},
month = oct
}
@inproceedings{hannan88iclp,
author = {John Hannan and Dale Miller},
title = {Uses of higher-order unification for implementing
program transformers},
editor = {Kenneth A. Bowen and Robert A. Kowalski},
booktitle = {Fifth International Logic Programming Conference},
address = {Seattle, Washington},
publisher = {MIT Press},
pages = {942--959},
month = aug,
year = {1988}
}
@techreport{hannan88tr,
author = {John Hannan and Dale Miller},
title = {Enriching a meta-language with higher-order features},
month = jun,
year = {1988},
institution = {University of Pennsylvania},
number = {MS-CIS-88-45},
url = {https://repository.upenn.edu/cis_reports/695/}
}
@incollection{hannan89meta,
author = {John Hannan and Dale Miller},
title = {A Meta-Logic for Functional Programming},
chapter = {24},
booktitle = {Meta-Programming in Logic Programming},
editor = {Harvey Abramson and M. H. Rogers},
publisher = {{MIT} Press},
pages = {453--476},
year = {1989},
series = {Computer Science and Intelligent Systems},
isbn = {0-262-51047-2},
note = {Proceedings of the 1988 Workshop on Meta-Programming
in Logic Programming, Bristol, UK}
}
@inproceedings{hannan89mpc,
author = {John Hannan and Dale Miller},
title = {Deriving mixed evaluation from standard evaluation for
a simple functional programming language},
booktitle = {1989 Intern.\ Conf.\ on Mathematics of Program
Construction},
editor = {Jan L. A. van de Snepscheut},
publisher = {Springer},
series = {LNCS},
volume = {375},
year = {1989},
pages = {239--255},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mpc89.pdf}
}
@inproceedings{hannan90lfp,
author = {John Hannan and Dale Miller},
title = {From Operational Semantics to Abstract Machines:
Preliminary Results},
booktitle = {Proceedings of the 1990 ACM Conference on Lisp and
Functional Programming},
editor = {M. Wand},
organization = {{ACM}},
publisher = {ACM Press},
pages = {323--332},
year = {1990},
doi = {10.1145/91556.91680}
}
@article{hannan92mscs,
author = {John Hannan and Dale Miller},
title = {From Operational Semantics to Abstract Machines},
journal = {Mathematical Structures in Computer Science},
volume = {2},
number = {4},
year = {1992},
pages = {415--459},
doi = {10.1017/S0960129500001559}
}
@inproceedings{heath15pxtp,
author = {Quentin Heath and Dale Miller},
title = {A framework for proof certificates in finite state
exploration},
booktitle = {Proceedings of the Fourth Workshop on Proof eXchange
for Theorem Proving},
year = {2015},
editor = {Cezary Kaliszyk and Andrei Paskevich},
number = {186},
series = {Electronic Proceedings in Theoretical Computer
Science},
pages = {11--26},
month = aug,
publisher = {Open Publishing Association},
doi = {10.4204/EPTCS.186.4},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/pxtp2015.pdf}
}
@inproceedings{heath17linearity,
author = {Quentin Heath and Dale Miller},
title = {A Proof Theory for Model Checking: An Extended
Abstract},
month = jan,
year = {2017},
booktitle = {Proceedings Fourth International Workshop on Linearity
(LINEARITY 2016)},
editor = {Iliano Cervesato and Maribel Fern\'andez},
volume = {238},
series = {EPTCS},
doi = {10.4204/EPTCS.238.1}
}
@article{heath19jar,
author = {Quentin Heath and Dale Miller},
title = {A proof theory for model checking},
year = {2019},
doi = {10.1007/s10817-018-9475-3},
journal = {J. of Automated Reasoning},
volume = {63},
number = {4},
pages = {857--885}
}
@inproceedings{hodas90iclp,
title = {Representing Objects in a Logic Programming Language
with Scoping Constructs},
author = {Joshua Hodas and Dale Miller},
year = {1990},
booktitle = {1990 International Conference in Logic Programming},
month = jun,
pages = {511--526},
publisher = {MIT Press},
editor = {David H. D. Warren and Peter Szeredi}
}
@inproceedings{hodas91lics,
author = {Joshua Hodas and Dale Miller},
title = {Logic Programming in a Fragment of Intuitionistic
Linear Logic: Extended Abstract},
booktitle = {6th Symp.\ on Logic in Computer Science},
editor = {G. Kahn},
address = {Amsterdam},
year = {1991},
month = jul,
pages = {32--42},
publisher = {IEEE}
}
@article{hodas94ic,
author = {Joshua Hodas and Dale Miller},
title = {Logic Programming in a Fragment of Intuitionistic
Linear Logic},
journal = {Information and Computation},
year = {1994},
volume = {110},
number = {2},
pages = {327--365},
doi = {10.1006/inco.1994.1036}
}
@inproceedings{leavens06gpce,
key = {Leavens and {\em et al.}},
author = {Gary T. Leavens and Jean-Raymond Abrial and Don Batory
and Michael Butler and Alessandro Coglio and Kathi
Fisler and Eric Hehner and Cliff Jones and Dale Miller
and Simon Peyton-Jones and Murali Sitaraman and Douglas
R. Smith and Aaron Stump},
title = {Roadmap for Enhanced Languages and Methods to Aid
Verification},
booktitle = {Fifth International Conference on Generative
Programming and Component Engineering (GPCE)},
pages = {221--235},
year = {2006},
month = oct,
organization = {ACM},
doi = {10.1145/1173706.1173740}
}
@inproceedings{liang07csl,
author = {Chuck Liang and Dale Miller},
title = {Focusing and Polarization in Intuitionistic Logic},
booktitle = {CSL 2007: Computer Science Logic},
editor = {J. Duparc and T. A. Henzinger},
volume = {4646},
series = {LNCS},
publisher = {Springer},
pages = {451--465},
year = {2007}
}
@unpublished{liang07report,
author = {Chuck Liang and Dale Miller},
title = {On focusing and polarities in linear logic and
intuitionistic logic},
url = {https://hal.inria.fr/inria-00167231/},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/focusli.pdf},
month = sep,
year = {2007},
note = {Extended version of accepted paper.}
}
@inproceedings{liang09lics,
author = {Chuck Liang and Dale Miller},
title = {A Unified Sequent Calculus for Focused Proofs},
year = {2009},
pages = {355--364},
booktitle = {24th Symp.\ on Logic in Computer Science},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/liang09lics.pdf}
}
@article{liang09tcs,
author = {Chuck Liang and Dale Miller},
title = {Focusing and Polarization in Linear, Intuitionistic,
and Classical Logics},
year = {2009},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
volume = {410},
number = {46},
pages = {4747--4768},
doi = {10.1016/j.tcs.2009.07.041},
note = {{Abstract} Interpretation and Logic Programming: A Special Issue in
Honor of Professor Giorgio Levi}
}
@article{liang11apal,
author = {Chuck Liang and Dale Miller},
title = {A Focused Approach to Combining Logics},
journal = {Annals of Pure and Applied Logic},
pages = {679--697},
volume = {162},
number = {9},
year = {2011},
doi = {10.1016/j.apal.2011.01.012},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lku.pdf}
}
@article{liang13apal,
author = {Chuck Liang and Dale Miller},
title = {Kripke Semantics and Proof Systems for Combining
Intuitionistic Logic and Classical Logic},
journal = {Annals of Pure and Applied Logic},
month = feb,
year = {2013},
doi = {10.1016/j.apal.2012.09.005},
volume = {164},
number = {2},
pages = {86--111},
url = {https://hal.inria.fr/hal-00787601}
}
@inproceedings{liang13lics,
author = {Chuck Liang and Dale Miller},
title = {Unifying Classical and Intuitionistic Logics for
Computational Control},
booktitle = {28th Symp.\ on Logic in Computer Science},
year = {2013},
editor = {Orna Kupferman},
pages = {283--292},
url = {https://hal.inria.fr/hal-00906299},
doi = {10.1109/LICS.2013.34}
}
@inproceedings{liang15lpar,
author = {Chuck Liang and Dale Miller},
title = {On Subexponentials, Synthetic Connectives, and
Multi-Level Delimited Control},
booktitle = {Logic for Programming, Artificial Intelligence, and
Reasoning (LPAR)},
year = {2015},
editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver
and Andrei Voronkov},
month = nov,
doi = {10.1007/978-3-662-48899-7\_21},
series = {LNCS},
number = {9450}
}
@incollection{liang24psh,
author = {Chuck Liang and Dale Miller},
title = {Focusing {Gentzen's} {LK} proof system},
booktitle = {Peter Schroeder-Heister on Proof-Theoretic Semantics},
editor = {Thomas Piecha and Kai Wehmeier},
series = {Outstanding Contributions to Logic},
publisher = {Springer},
pages = {275--313},
month = feb,
year = {2024},
doi = {10.1007/978-3-031-50981-0\_9}
}
@inproceedings{libal16fscd,
author = {Tomer Libal and Dale Miller},
title = {Functions-as-constructors Higher-order Unification},
booktitle = {1st International Conference on Formal Structures for
Computation and Deduction (FSCD 2016)},
year = {2016},
editor = {D. Kesner and B. Pientka},
pages = {26:1--26:17},
doi = {10.4230/LIPIcs.FSCD.2016.0},
isbn = {978-3-9597701-0-1},
pdf = {https://hal.inria.fr/hal-01379683/file/fscd16.pdf}
}
@article{libal22amai,
author = {Tomer Libal and Dale Miller},
title = {Functions-as-constructors higher-order unification:
extended pattern unification},
journal = {Annals of Mathematics and Artificial Intelligence},
year = {2022},
pages = {455--479},
volume = {90},
number = {5},
note = {Appears in the \emph{Special Issue on Theoretical and
Practical Aspects of Unification}},
doi = {10.1007/s10472-021-09774-y}
}
@inproceedings{manighetti21types,
author = {Matteo Manighetti and Dale Miller and Alberto
Momigliano},
title = {{Two Applications of Logic Programming to Coq}},
booktitle = {26th International Conference on Types for Proofs and
Programs (TYPES 2020)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
isbn = {978-3-9597718-2-5},
issn = {1868-8969},
year = {2021},
volume = {188},
editor = {Ugo de'Liguoro and Stefano Berardi and Thorsten
Altenkirch},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r
Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13889},
doi = {10.4230/LIPIcs.TYPES.2020.10}
}
@techreport{manighetti22hal,
author = {Matteo Manighetti and Dale Miller},
title = {Computational logic based on linear logic and fixed
points},
institution = {HAL},
year = {2022},
number = {hal-03579451},
url = {https://hal.inria.fr/hal-03579451}
}
@techreport{manighetti23arxiv,
author = {Matteo Manighetti and Dale Miller},
title = {Peano Arithmetic and mu{MALL}},
institution = {arXiv},
year = {2023},
number = {arXiv:2312.13634},
url = {https://arxiv.org/abs/2312.13634}
}
@misc{manighetti25fi,
author = {Matteo Manighetti and Dale Miller},
title = {Peano Arithmetic and $\mu${MALL}},
year = {2025},
note = {To appear in Fundam. Informaticae. Prepublication
draft areas as arXiv:2312.13634},
url = {https://arxiv.org/abs/2312.13634}
}
@inproceedings{marin16aiml,
author = {Sonia Marin and Dale Miller and Marco Volpe},
title = {A focused framework for emulating modal proof
systems},
url = {https://hal.archives-ouvertes.fr/hal-01379624},
booktitle = {{11th Conference on Advances in Modal Logic}},
address = {Budapest, Hungary},
editor = {Lev Beklemishev and St{\'e}phane Demri and Andr{\'a}s
M{\'a}t{\'e}},
publisher = {{College Publications}},
series = {Advances in Modal Logic},
number = {11},
pages = {469--488},
year = {2016},
month = aug,
keywords = {Focusing ; Labeled proof systems ; Modal logic ;
Sequent calculi},
pdf = {https://hal.archives-ouvertes.fr/hal-01379624/file/aiml2016.pdf},
hal_id = {hal-01379624},
hal_version = {v1}
}
@article{marin22apal,
author = {Sonia Marin and Dale Miller and Elaine Pimentel and
Marco Volpe},
title = {From axioms to synthetic inference rules via
focusing},
journal = {Annals of Pure and Applied Logic},
doi = {10.1016/j.apal.2022.103091},
volume = {173},
number = {5},
pages = {1--32},
year = {2022}
}
@article{mcdowell00tcs,
author = {Raymond McDowell and Dale Miller},
title = {Cut-elimination for a logic with definitions and
induction},
journal = {Theoretical Computer Science},
volume = {232},
pages = {91--119},
year = {2000},
doi = {10.1016/S0304-3975(99)00171-1}
}
@article{mcdowell02tocl,
author = {Raymond McDowell and Dale Miller},
title = {Reasoning with Higher-Order Abstract Syntax in a
Logical Framework},
journal = {ACM Trans.\ on Computational Logic},
year = {2002},
volume = {3},
number = {1},
pages = {80--136},
doi = {10.1145/504077.504080},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mcdowell01.pdf}
}
@article{mcdowell03tcs,
author = {Raymond McDowell and Dale Miller and Catuscia
Palamidessi},
title = {Encoding transition systems in sequent calculus},
journal = {Theoretical Computer Science},
year = {2003},
volume = {294},
number = {3},
pages = {411--437},
doi = {10.1016/S0304-3975(01)00168-2}
}
@article{mcdowell96llw,
author = {Raymond McDowell and Dale Miller and Catuscia
Palamidessi},
title = {Encoding Transition Systems in Sequent Calculus:
Preliminary Report},
journal = {ENTCS},
volume = {3},
year = {1996}
}
@inproceedings{mcdowell97lics,
author = {Raymond McDowell and Dale Miller},
title = {A Logic for Reasoning with Higher-Order Abstract
Syntax},
year = {1997},
booktitle = {12th Symp.\ on Logic in Computer Science},
editor = {Glynn Winskel},
month = jul,
pages = {434--445},
address = {Warsaw, Poland},
organization = {IEEE Computer Society Press}
}
@unpublished{miller.sml,
author = {Dale Miller},
title = {Semantics of a simple meta-logic},
month = mar,
year = {1990},
note = {Unpublished draft}
}
@inproceedings{miller00cl,
author = {Dale Miller},
title = {Abstract Syntax for Variable Binders: An Overview},
booktitle = {CL 2000: Computational Logic},
pages = {239--253},
year = {2000},
editor = {John Lloyd and {\em et al.}},
number = {1861},
series = {LNAI},
publisher = {Springer},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/cl2000.pdf}
}
@inproceedings{miller01entcs,
author = {Dale Miller},
title = {Encoding Generic Judgments: Preliminary results},
series = {ENTCS},
volume = {58},
publisher = {Elsevier Science Publishers},
editor = {R. L. Crole and S. J. Ambler and A. Momigliano},
booktitle = {Proceedings of the MERLIN 2001 Workshop, Siena},
year = {2001}
}
@inproceedings{miller02amast,
author = {Dale Miller},
title = {Higher-order quantification and proof search},
booktitle = {Proceedings of AMAST 2002},
pages = {60--74},
year = {2002},
editor = {H\'el\`ene Kirchner and Christophe Ringeissen},
number = {2422},
series = {LNCS},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/amast02.pdf}
}
@inproceedings{miller02fsttcs,
author = {Dale Miller and Alwen Tiu},
title = {Encoding Generic Judgments},
booktitle = {Proceedings of FSTTCS},
pages = {18--32},
year = {2002},
publisher = {Springer},
series = {LNCS},
number = {2556},
month = dec,
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fsttcs02.pdf}
}
@misc{miller02llw,
author = {Dale Miller},
title = {Higher-order quantification and proof search: an
extended abstract},
month = jul,
year = {2002},
note = {Presented at Linear Logic 2002, FLoC, Copenhagen}
}
@inproceedings{miller02tableaux,
author = {Dale Miller and Elaine Pimentel},
title = {Using linear logic to reason about sequent systems},
pages = {2--23},
editor = {Uwe Egly and Christian G. Ferm{\"u}ller},
booktitle = {International Conference on Automated Reasoning with
Analytic Tableaux and Related Methods},
publisher = {Springer},
series = {LNCS},
volume = {2381},
year = {2002},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tableaux02.pdf}
}
@inproceedings{miller03fcs,
author = {Dale Miller},
title = {Encryption as an Abstract Data-Type: An extended
abstract},
booktitle = {Proceedings of FCS'03: Foundations of Computer
Security},
editor = {Iliano Cervesato},
pages = {18--29},
year = {2003},
series = {ENTCS},
volume = {84},
publisher = {Elsevier},
doi = {10.1016/S1571-0661(04)80841-7}
}
@inproceedings{miller03lics,
author = {Dale Miller and Alwen Tiu},
title = {A Proof Theory for Generic Judgments: An extended
abstract},
booktitle = {18th Symp.\ on Logic in Computer Science},
pages = {118--127},
editor = {Phokion Kolaitis},
year = {2003},
month = jun,
publisher = {IEEE},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics03.pdf}
}
@inproceedings{miller03tphols,
author = {Dale Miller},
title = {Reasoning about proof search specifications: An
abstract},
booktitle = {Theorem Proving in Higher Order Logics: 16th
International Conference, TPHOLs 2003},
pages = {204},
year = {2003},
volume = {2758},
series = {LNCS},
publisher = {Springer},
note = {Invited speaker},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tphols03talk.pdf}
}
@inproceedings{miller03unif,
author = {Dale Miller},
title = {Definitions, Unification, and the Sequent Calculus},
booktitle = {Proceedings of the 17th International Workshop on
Unification, UNIF'03},
pages = {1--2},
year = {2003},
editor = {J. Levy and M. Kohlhase and J. Niehren and M.
Villaret},
series = {Technical Report DSIC-II/12/03},
month = jun,
organization = {Departamento de Sistemas Inform{\`a}tics i
Computaci{\'o} Universidad Polit{\`e}cnica de
Val{\`e}ncia},
note = {Invited talk}
}
@inproceedings{miller03wollic,
author = {Dale Miller},
title = {Encryption as an abstract data type},
booktitle = {WoLLIC'2003, 10th Workshop on Logic, Language,
Information and Computation},
series = {ENTCS},
volume = {84},
publisher = {Elsevier},
editor = {Ruy de Queiroz and Elaine Pimentel and Lucilia
Figueiredo},
note = {Invited talk},
year = {2003}
}
@inproceedings{miller04csl,
author = {Dale Miller},
title = {Bindings, mobility of bindings, and the
$\nabla$-quantifier},
booktitle = {18th International Conference on Computer Science
Logic {(CSL)} 2004},
pages = {24},
year = {2004},
editor = {Jerzy Marcinkowski and Andrzej Tarlecki},
volume = {3210},
series = {LNCS},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/csl04talk.pdf},
doi = {10.1007/978-3-540-30124-0\_4}
}
@incollection{miller04lc,
author = {Dale Miller and Elaine Pimentel},
title = {Linear logic as a framework for specifying sequent
calculus},
booktitle = {Logic Colloquium '99: Proceedings of the Annual
European Summer Meeting of the Association for Symbolic
Logic},
publisher = {A K Peters Ltd},
series = {Lecture Notes in Logic},
editor = {Jan van Eijck and Vincent van Oostrom and Albert
Visser},
pages = {111--135},
year = {2004}
}
@incollection{miller04llcs,
author = {Dale Miller},
editor = {Thomas Ehrhard and Jean-Yves Girard and Paul Ruet and
Phil Scott},
booktitle = {Linear Logic in Computer Science},
title = {Overview of linear logic programming},
publisher = {Cambridge University Press},
series = {London Mathematical Society Lecture Note},
volume = {316},
year = {2004},
pages = {119--150}
}
@inproceedings{miller05apc,
author = {Dale Miller},
title = {A Proof Theoretic Approach to Operational Semantics},
year = {2005},
pages = {172--175},
booktitle = {Algebraic Process Calculi: The First Twenty Five Years
and Beyond},
editor = {Luca Aceto and Andrew D. Gordon},
month = aug,
organization = {Bertinoro, Italy},
url = {ftp://ftp.daimi.au.dk/pub/BRICS/BRICS/Reports/NS/05/3/BRICS-NS-05-3.pdf}
}
@inproceedings{miller05galop,
author = {Dale Miller and Alexis Saurin},
title = {A game semantics for proof search: Preliminary
results},
booktitle = {GaLoP 2005: Games for Logic and Programming
Languages},
editor = {Dan Ghica and Guy McCusker},
year = {2005}
}
@inproceedings{miller05mfps,
author = {Dale Miller and Alexis Saurin},
title = {A game semantics for proof search: Preliminary
results},
booktitle = {Proceedings of the 21st Annual Conference on
Mathematical Foundations of Programming Semantics (MFPS
XXI)},
editor = {M. Escard\'{o} and A. Jung and M. Mislove},
year = {2005},
pages = {543--563},
volume = {155},
series = {ENTCS},
publisher = {Elsevier},
doi = {10.1016/j.entcs.2005.11.072}
}
@article{miller05tocl,
author = {Dale Miller and Alwen Tiu},
title = {A proof theory for generic judgments},
journal = {ACM Trans.\ on Computational Logic},
editor = {Phokion Kolaitis},
month = oct,
volume = {6},
number = {4},
doi = {10.1145/1094622.1094628},
pages = {749--783},
publisher = {ACM Press},
address = {New York, NY, USA},
year = {2005}
}
@misc{miller06alp,
author = {Dale Miller},
title = {Logic and Logic Programming: {A} Personal Account},
howpublished = {ALP Newsletter},
month = feb,
year = {2006},
note = {Vol.\ 19, No.\ 1},
url = {https://www.cs.kuleuven.ac.be/~dtai/projects/ALP/newsletter/feb06/nav/articles/Dale/dale.pdf}
}
@inproceedings{miller06ijcar,
author = {Dale Miller},
title = {Representing and reasoning with operational
semantics},
booktitle = {Proceedings of IJCAR: International Joint Conference
on Automated Reasoning},
month = aug,
year = {2006},
pages = {4--20},
editor = {U. Furbach and N. Shankar},
series = {LNAI},
volume = {4130},
publisher = {Springer},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ijcar06.pdf}
}
@inproceedings{miller06mfps,
author = {Dale Miller and Alexis Saurin},
title = {A game semantics for proof search: Preliminary
results},
booktitle = {Proceedings of the Mathematical Foundations of
Programming Semantics (MFPS05)},
pages = {543--563},
number = {155},
series = {ENTCS},
year = {2006},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mfps05.pdf}
}
@inproceedings{miller06ppdp,
author = {Dale Miller},
title = {Collection analysis for {Horn} clause programs},
booktitle = {Proceedings of PPDP 2006: 8th International ACM
SIGPLAN Conference on Principles and Practice of
Declarative Programming},
month = jul,
pages = {179--188},
year = {2006},
doi = {10.1145/1140335.1140357}
}
@inproceedings{miller07csla,
author = {Dale Miller and Vivek Nigam},
title = {Incorporating tables into proofs},
booktitle = {CSL 2007: Computer Science Logic},
editor = {J. Duparc and T. A. Henzinger},
year = {2007},
volume = {4646},
series = {LNCS},
publisher = {Springer},
pages = {466--480},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/csl07nigam.pdf},
doi = {10.1007/978-3-540-74915-8\_35}
}
@inproceedings{miller07cslb,
author = {Dale Miller and Alexis Saurin},
title = {From proofs to focused proofs: a modular proof of
focalization in Linear Logic},
booktitle = {CSL 2007: Computer Science Logic},
editor = {J. Duparc and T. A. Henzinger},
volume = {4646},
series = {LNCS},
publisher = {Springer},
pages = {405--419},
year = {2007},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/csl07saurin.pdf}
}
@incollection{miller08andrews,
author = {Dale Miller},
title = {A Proof-Theoretic Approach to the Static Analysis of
Logic Programs},
booktitle = {Reasoning in Simple Type Theory: Festschrift in Honor
of Peter B. Andrews on His 70th Birthday},
publisher = {College Publications},
editor = {Christoph Benzm{\"u}ller and Chad E. Brown and
J{\"o}rg Siekmann and Richard Statman},
year = {2008},
series = {Studies in Logic},
number = {17},
pages = {423--442},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/andrews-festschrift-2007.pdf}
}
@article{miller08beatcs,
author = {Dale Miller},
title = {Formalizing operational semantic specifications in
logic},
journal = {Concurrency Column of the Bulletin of the EATCS},
year = {2008},
editor = {Luca Aceto},
month = oct,
pdf = {https://www.ru.is/faculty/luca/BEATCS/miller.pdf}
}
@unpublished{miller08unp,
author = {Dale Miller and Vivek Nigam},
title = {Proofs with tables},
note = {Available via the authors web pages},
year = {2008}
}
@inproceedings{miller09wflp,
author = {Dale Miller},
title = {Formalizing Operational Semantic Specifications in
Logic},
booktitle = {Proceedings of the 17th International Workshop on
Functional and (Constraint) Logic Programming (WFLP
2008)},
volume = {246},
pages = {147--165},
year = {2009},
month = aug,
doi = {10.1016/j.entcs.2009.07.020}
}
@inproceedings{miller10aplas,
author = {Dale Miller},
title = {Reasoning about Computations Using Two-Levels of
Logic},
year = {2010},
booktitle = {{P}roceedings of the 8th {A}sian {S}ymposium on
{P}rogramming {L}anguages and {S}ystems ({APLAS}'10)},
editor = {K. Ueda},
number = {6461},
series = {LNCS},
pages = {34--46},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/aplas10.pdf}
}
@inproceedings{miller10bcs,
author = {Dale Miller},
title = {Finding unity in computational logic},
year = {2010},
booktitle = {Proceedings of the 2010 ACM-BCS Visions of Computer
Science Conference},
series = {ACM-BCS '10},
month = apr,
pages = {3:1--3:13},
publisher = {British Computer Society},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/unity2010.pdf}
}
@inproceedings{miller11cpp,
author = {Dale Miller},
title = {A proposal for broad spectrum proof certificates},
booktitle = {CPP: First International Conference on Certified
Programs and Proofs},
year = {2011},
editor = {J.-P. Jouannaud and Z. Shao},
series = {LNCS},
volume = {7086},
pages = {54--69},
doi = {10.1007/978-3-642-25379-9\_6},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/cpp11.pdf}
}
@unpublished{miller11erc,
author = {Dale Miller},
title = {{ProofCert}: Broad Spectrum Proof Certificates},
note = {An ERC Advanced Grant funded for the five years
2012-2016},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/ProofCert.pdf},
month = feb,
year = {2011}
}
@book{miller12proghol,
author = {Dale Miller and Gopalan Nadathur},
title = {Programming with Higher-Order Logic},
publisher = {Cambridge University Press},
year = {2012},
month = jun,
doi = {10.1017/CBO9781139021326}
}
@inproceedings{miller13cpp,
author = {Dale Miller and Alwen Tiu},
title = {Extracting Proofs from Tabled Proof Search},
booktitle = {Certified Programs and Proofs},
year = {2013},
editor = {Georges Gonthier and Michael Norrish},
month = dec,
publisher = {Springer},
series = {LNCS},
number = {8307},
pages = {194--210},
url = {https://hal.inria.fr/hal-00863561/},
address = {Melburne, Australia}
}
@inproceedings{miller13lfmtp,
author = {Dale Miller},
title = {Foundational Proof Certificates: Making Proof
Universal and Permanent},
booktitle = {Proceedings of the 2013 ACM SIGPLAN Workshop on
Logical Frameworks~\& Meta-Languages: Theory~\&
Practice, LFMTP'13},
pages = {1},
year = {2013},
editor = {Alberto Momigliano and Brigitte Pientka and Randy
Pollack},
month = sep,
publisher = {ACM},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lfmtp13.pdf},
doi = {10.1145/2503887.2503894}
}
@article{miller13tcs,
author = {Dale Miller and Elaine Pimentel},
title = {A formal framework for specifying sequent calculus
proof systems},
journal = {Theoretical Computer Science},
year = {2013},
doi = {10.1016/j.tcs.2012.12.008},
volume = {474},
pages = {98--116}
}
@techreport{miller13tr,
author = {Dale Miller and Alwen Tiu},
title = {Extracting Proofs from Tabled Proof Search: Extended
version},
institution = {INRIA-HAL},
year = {2013},
url = {https://hal.inria.fr/hal-00863561}
}
@inproceedings{miller14clmps,
author = {Dale Miller},
title = {Communicating and trusting proofs: The case for broad
spectrum proof certificates},
booktitle = {Logic, Methodology, and Philosophy of Science.
Proceedings of the Fourteenth International Congress},
year = {2014},
editor = {P. Schroeder-Heister and W. Hodges and G. Heinzmann
and P. E. Bour},
pages = {323--342},
publisher = {College Publications}
}
@incollection{miller15appa,
author = {Dale Miller},
title = {Foundational Proof Certificates},
pages = {150--163},
year = {2015},
month = jan,
booktitle = {All about Proofs, Proofs for All},
editor = {David Delahaye and Bruno Woltzenlogel Paleo},
publisher = {College Publications},
address = {London, UK},
series = {Mathematical Logic and Foundations},
volume = {55},
isbn = {978-1-84890-166-7},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/appa2014.pdf}
}
@inproceedings{miller15lopstr,
author = {Dale Miller},
title = {Proof Checking and Logic Programming},
booktitle = {Logic-Based Program Synthesis and Transformation
(LOPSTR) 2015},
year = {2015},
editor = {Moreno Falaschi},
doi = {10.1007/978-3-319-27436-2\_1},
series = {LNCS},
number = {9527},
publisher = {Springer},
pages = {3--17}
}
@inproceedings{miller15lpar,
author = {Dale Miller and Marco Volpe},
title = {Focused labeled proof systems for modal logic},
booktitle = {Logic for Programming, Artificial Intelligence, and
Reasoning (LPAR)},
year = {2015},
editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver
and Andrei Voronkov},
series = {LNCS},
number = {9450},
doi = {10.1007/978-3-662-48899-7\_19},
pages = {266--280},
month = nov
}
@inproceedings{miller15ppdp,
author = {Dale Miller},
title = {Proof Checking and Logic Programming},
booktitle = {ACM SIGPLAN Conference on Principles and Practice of
Declarative Programming (PPDP)},
year = {2015},
editor = {Elvira Albert},
pages = {18},
month = jul,
doi = {10.1145/2790449.2790510},
publisher = {ACM}
}
@incollection{miller17epsa,
booktitle = {Towards an Encyclopaedia of Proof Systems},
editor = {Bruno Woltzenlogel Paleo},
title = {Focused {LK}},
author = {Dale Miller},
pages = {66--67},
publisher = {College Publications},
address = {London, UK},
url = {https://github.com/ProofSystem/Encyclopedia/blob/master/main.pdf},
year = {2017},
month = jan,
edition = {1}
}
@incollection{miller17epsb,
booktitle = {Towards an Encyclopaedia of Proof Systems},
editor = {Bruno Woltzenlogel Paleo},
title = {Focused {LJ}},
author = {Dale Miller},
pages = {68--69},
publisher = {College Publications},
address = {London, UK},
url = {https://github.com/ProofSystem/Encyclopedia/blob/master/main.pdf},
year = {2017},
month = jan,
edition = {1}
}
@incollection{miller17epsc,
booktitle = {Towards an Encyclopaedia of Proof Systems},
editor = {Bruno Woltzenlogel Paleo},
title = {Expansion Proofs},
author = {Dale Miller},
pages = {18},
publisher = {College Publications},
address = {London, UK},
url = {https://github.com/ProofSystem/Encyclopedia/blob/master/main.pdf},
year = {2017},
month = jan,
edition = {1}
}
@article{miller17fac,
author = {Dale Miller},
title = {Proof checking and logic programming},
journal = {Formal Aspects of Computing},
year = {2017},
pages = {383--399},
volume = {29},
number = {3},
doi = {10.1007/s00165-016-0393-z}
}
@misc{miller18hapop,
author = {Dale Miller},
title = {{Influences between logic programming and proof
theory}},
url = {https://inria.hal.science/hal-01900891},
howpublished = {{HaPoP 2018: Fourth Symposium on the History and
Philosophy of Programming}},
year = {2018},
month = mar
}
@inproceedings{miller18types,
author = {Dale Miller},
url = {https://hal.inria.fr/hal-01615681},
title = {{Mechanized Metatheory Revisited: An Extended Abstract
(Invited Paper)}},
booktitle = {22nd International Conference on Types for Proofs and
Programs (TYPES 2016)},
pages = {1:1--1:16},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
year = {2018},
volume = {97},
editor = {Silvia Ghilezan and Herman Geuvers and Jelena
Ivetić},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
doi = {10.4230/LIPIcs.TYPES.2016.1}
}
@incollection{miller19catuscia,
author = {Dale Miller},
title = {My colleague, wife, and friend},
booktitle = {The Art of Modelling Computational Systems: A Journey
from Logic and Concurrency to Security and Privacy.
Essays Dedicated to Catuscia Palamidessi on the
Occasion of Her 60th Birthday},
publisher = {pub-sv},
year = {2019},
editor = {M\'ario S. Alvim and Kostas Chatzikokolakis and Carlos
Olarte and Frank Valencia},
number = {11769},
series = {lncs},
pages = {xv--xvii},
doi = {10.1007/978-3-030-31175-9},
month = nov
}
@article{miller19jar,
author = {Dale Miller},
title = {Mechanized Metatheory Revisited},
journal = {Journal of Automated Reasoning},
year = {2019},
month = oct,
volume = {63},
number = {3},
doi = {10.1007/s10817-018-9483-3},
pages = {625--665}
}
@inproceedings{miller20icdcit,
author = {Dale Miller},
title = {A distributed and trusted web of formal proofs},
booktitle = {Distributed Computing and Internet Technology
(ICDCIT)},
year = {2020},
editor = {D. V. Hung and M. D'Souza},
number = {11969},
series = {LNCS},
publisher = {Springer},
pages = {21--40},
doi = {10.1007/978-3-030-36987-3\_2}
}
@incollection{miller20scedrov,
author = {Dale Miller},
title = {Andre and the Early Days of Penn’s Logic and
Computation Group},
booktitle = {Logic, Language, and Security},
publisher = {pub-sv},
year = {2020},
editor = {Vivek Nigam et al.},
number = {12300},
series = {lncs},
doi = {10.1007/978-3-030-62077-6_6}
}
@article{miller21pt,
author = {Dale Miller},
title = {Reciprocal influences between logic programming and
proof theory},
journal = {Philosophy \& Technology},
volume = {34},
number = {1},
pages = {75--104},
month = mar,
year = {2021},
doi = {10.1007/s13347-019-00370-x},
publisher = {Springer}
}
@article{miller22amai,
author = {Dale Miller and Alexandre Viel},
title = {Proof search when equality is a logical connective},
journal = {Annals of Mathematics and Artificial Intelligence},
year = {2022},
volume = {90},
number = {5},
pages = {523--535},
doi = {10.1007/s10472-021-09764-0},
note = {\emph{Special Issue on Theoretical and Practical
Aspects of Unification}}
}
@misc{miller22blog,
author = {Dale Miller},
title = {{LK} vs {LJ}: An origin story for linear logic},
howpublished = {Proof Theory Blog},
month = jul,
year = {2022},
url = {https://prooftheory.blog/2022/07/06/lk-vs-lj-an-origin-story-for-linear-logic/}
}
@article{miller22tplp,
author = {Dale Miller},
title = {A Survey of the Proof-Theoretic Foundations of Logic
Programming},
journal = {Theory and Practice of Logic Programming},
volume = {22},
number = {6},
year = {2022},
month = oct,
pages = {859--904},
doi = {10.1017/S1471068421000533},
publisher = {Cambridge University Press},
note = {Published online November 2021}
}
@techreport{miller22tr,
author = {Dale Miller and Jui-Hsuan Wu},
title = {A positive perspective on term representations:
Extended paper},
institution = {Inria},
year = {2022},
url = {https://hal.inria.fr/hal-03843587}
}
@unpublished{miller22unp,
author = {Dale Miller},
title = {Proof theory, proof search, and logic programming},
note = {Unpublished monograph},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/mpri/ln2022-v1.pdf},
month = dec,
year = {2022}
}
@inproceedings{miller23csl,
author = {Dale Miller and Jui-Hsuan Wu},
title = {A positive perspective on term representations},
booktitle = {31st EACSL Annual Conference on Computer Science Logic
(CSL 2023)},
year = {2023},
editor = {Bartek Klin and Elaine Pimentel},
volume = {252},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
doi = {10.4230/LIPIcs.CSL.2023.3},
pages = {3:1--3:21},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany}
}
@inproceedings{miller23lics,
author = {Dale Miller},
title = {A system of inference based on proof search: an
extended abstract},
booktitle = {Thirty-Eighth Annual ACM/IEEE Symposium on Logic in
Computer Science (LICS 2023)},
year = {2023},
editor = {Igor Walukiewicz},
doi = {10.1109/LICS56636.2023.10175827},
pages = {1--11}
}
@article{miller24tplp,
author = {Dale Miller and Alberto Momigliano},
title = {Property-Based Testing by Elaborating Proof Outlines},
journal = {Theory and Practice of Logic Programming},
year = {2024},
month = nov,
doi = {10.1017/S1471068424000176},
pages = {1123--1162},
volume = {24},
number = {6}
}
@inproceedings{miller82,
author = {Dale A. Miller and Eve Longini Cohen and Peter B.
Andrews},
title = {A Look at {TPS}},
booktitle = {Sixth Conference on Automated Deduction},
address = {New York},
publisher = {Springer},
year = {1982},
editor = {Donald W. Loveland},
series = {LNCS},
volume = {138},
pages = {50--69}
}
@phdthesis{miller83,
author = {Dale Miller},
title = {Proofs in Higher-order Logic},
school = {Carnegie-Mellon University},
month = aug,
year = {1983},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/th.pdf}
}
@inproceedings{miller84,
title = {Expansion Tree Proofs and Their Conversion to Natural
Deduction Proofs},
author = {Dale Miller},
booktitle = {Seventh Conference on Automated Deduction},
address = {Napa CA},
month = may,
year = {1984},
pages = {375--393},
publisher = {Springer},
series = {LNCS},
volume = {170},
editor = {R. E. Shostak}
}
@unpublished{miller85,
title = {A computational logic approach to syntax and
semantics},
author = {Dale Miller and Gopalan Nadathur},
month = may,
year = {1985},
note = {Presented at the Tenth Symposium of the Mathematical
Foundations of Computer Science, IBM Japan}
}
@inproceedings{miller86aaai,
title = {An integration of resolution and natural deduction
theorem proving},
author = {Dale Miller and Amy Felty},
booktitle = {National Conference on Artificial Intelligence
(AAAI-86)},
address = {Philadelphia, PA},
month = aug,
year = {1986},
editor = {Tom Kehler and Stan Rosenschein and Robert Filman and
Peter F. Patel-Schneider},
pages = {198--202}
}
@inproceedings{miller86acl,
author = {Dale Miller and Gopalan Nadathur},
title = {Some Uses of Higher-Order Logic in Computational
Linguistics},
booktitle = {Proceedings of the 24th Annual Meeting of the
Association for Computational Linguistics},
pages = {247--255},
year = {1986},
publisher = {Association for Computational Linguistics, Morristown,
New Jersey},
doi = {10.3115/981131.981165}
}
@inproceedings{miller86iclp,
author = {Dale Miller and Gopalan Nadathur},
title = {Higher-Order Logic Programming},
booktitle = {{Proceedings of the Third International Logic
Programming Conference}},
pages = {448--462},
editor = {Ehud Shapiro},
address = {London},
month = jun,
year = {1986},
series = {LNCS},
volume = {225},
publisher = {Springer},
doi = {10.1007/3-540-16492-8\_94}
}
@inproceedings{miller86slp,
author = {Dale Miller},
title = {A Theory of Modules for Logic Programming},
booktitle = {Third Annual IEEE Symposium on Logic Programming},
address = {Salt Lake City, Utah},
editor = {Robert M. Keller},
pages = {106--114},
month = sep,
year = {1986}
}
@inproceedings{miller87lics,
author = {Dale Miller and Gopalan Nadathur and Andre Scedrov},
title = {Hereditary {Harrop} Formulas and Uniform Proof
Systems},
booktitle = {2nd Symp.\ on Logic in Computer Science},
pages = {98--105},
editor = {David Gries},
address = {Ithaca, NY},
month = jun,
year = {1987}
}
@inproceedings{miller87lmps,
author = {Dale Miller},
title = {Hereditary {Harrop} formulas and logic programming},
booktitle = {Proceedings of the VIII International Congress of
Logic, Methodology, and Philosophy of Science},
address = {Moscow},
pages = {153--156},
month = aug,
year = {1987}
}
@unpublished{miller87lp,
author = {Dale Miller and Gopalan Nadathur},
title = {{$\lambda$Prolog Version 2.6}},
month = aug,
year = {1987},
note = {Distribution in C-Prolog sources}
}
@article{miller87sl,
author = {Dale Miller},
title = {A Compact Representation of Proofs},
journal = {Studia Logica},
volume = {46},
number = {4},
pages = {347--370},
year = {1987},
doi = {10.1007/BF00370646}
}
@inproceedings{miller87slp,
author = {Dale Miller and Gopalan Nadathur},
title = {A Logic Programming Approach to Manipulating Formulas
and Programs},
booktitle = {IEEE Symposium on Logic Programming},
address = {San Francisco},
editor = {Seif Haridi},
pages = {379--388},
month = sep,
year = {1987},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/slp87.pdf}
}
@techreport{miller88asflp,
author = {Dale Miller},
title = {Logic Programming Based on Higher-Order Hereditary
{Harrop} Formulas},
institution = {Computer Science Department, University of
Pennsylvania},
month = sep,
year = {1988},
number = {MS-CIS-88-77},
note = {Transparencies for lectures at the Advanced School on
Foundations of Logic Programming, Algehro, Sardinia}
}
@unpublished{miller88lp,
author = {Dale Miller and Gopalan Nadathur},
title = {{$\lambda$Prolog Version 2.7}},
month = jul,
year = {1988},
note = {Distribution in C-Prolog and Quintus sources},
url = {https://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/lang/prolog/impl/prolog/lp/}
}
@inproceedings{miller89banff,
author = {Dale Miller},
title = {A Logic Programming Language with Lambda-Abstraction,
Function Variables, and Simple Unification: Extended
Abstract},
booktitle = {Proceedings of the 1989 Banff meeting on
{``}Higher-Orders{''}},
month = sep,
year = {1989},
editor = {Graham M. Birtwistle},
address = {Banff, Canada}
}
@inproceedings{miller89iclp,
author = {Dale Miller},
title = {Lexical Scoping as Universal Quantification},
editor = {G. Levi and M. Martelli},
booktitle = {{Sixth International Logic Programming Conference}},
address = {Lisbon, Portugal},
publisher = {MIT Press},
pages = {268--283},
month = jun,
year = {1989},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/iclp89.pdf}
}
@article{miller89jlp,
author = {Dale Miller},
title = {A logical analysis of modules in logic programming},
journal = {Journal of Logic Programming},
volume = {6},
number = {1-2},
month = jan,
year = {1989},
pages = {79--108},
doi = {10.1016/0743-1066(89)90031-9}
}
@incollection{miller90abs,
author = {Dale Miller},
title = {Abstractions in logic programming},
booktitle = {Logic and Computer Science},
editor = {Piergiorgio Odifreddi},
publisher = {Academic Press},
pages = {329--359},
year = {1990},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/AbsInLP.pdf}
}
@inproceedings{miller90tr,
author = {Dale Miller},
title = {An Extension to {ML} to Handle Bound Variables in Data
Structures: Preliminary Report},
month = jun,
year = {1990},
booktitle = {Proceedings of the Logical Frameworks BRA Workshop},
address = {Antibes, France},
pages = {323--335},
note = {Available as UPenn CIS technical report MS-CIS-90-59},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mll.pdf}
}
@article{miller91alp,
author = {Dale Miller},
title = {Proof Theory as an Alternative to Model Theory},
journal = {Newsletter of the Association for Logic Programming},
year = {1991},
month = aug,
volume = {4},
number = {3},
note = {Guest editorial.},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ProofTheoryAsAlternative.html}
}
@article{miller91apal,
author = {Dale Miller and Gopalan Nadathur and Frank Pfenning
and Andre Scedrov},
title = {Uniform Proofs as a Foundation for Logic Programming},
journal = {Annals of Pure and Applied Logic},
year = {1991},
volume = {51},
number = {1--2},
pages = {125--157},
doi = {10.1016/0168-0072(91)90068-W}
}
@inproceedings{miller91elp,
author = {Dale Miller},
editor = {Lars-Henrik Eriksson and Lars Halln{\"a}s and Peter
Schroeder-Heister},
title = {A Logic Programming Language with Lambda-Abstraction,
Function Variables, and Simple Unification},
booktitle = {{Extensions of Logic Programming: Second International
Workshop, ELP '91, Stockholm, Sweden, January 27-29,
1991. Proceedings}},
publisher = {Springer},
series = {LNAI},
volume = {475},
year = {1991},
pages = {253--281}
}
@inproceedings{miller91iclp,
author = {Dale Miller},
title = {Unification of Simply Typed Lambda-Terms as Logic
Programming},
editor = {Koichi Furukawa},
booktitle = {Eighth International Logic Programming Conference},
address = {Paris, France},
publisher = {MIT Press},
month = jun,
year = {1991},
pages = {255--269}
}
@article{miller91jlc,
author = {Dale Miller},
title = {A Logic Programming Language with Lambda-Abstraction,
Function Variables, and Simple Unification},
journal = {J. of Logic and Computation},
volume = {1},
number = {4},
pages = {497--536},
year = {1991},
doi = {10.1093/logcom/1.4.497}
}
@incollection{miller92encyclopedia,
author = {Dale Miller},
title = {Logic, Higher-order},
booktitle = {Second Edition of the Encyclopedia of Artificial
Intelligence},
publisher = {Wiley},
year = {1992},
editor = {S. Shapiro}
}
@article{miller92jsc,
author = {Dale Miller},
title = {Unification under a mixed prefix},
year = {1992},
journal = {Journal of Symbolic Computation},
pages = {321--358},
volume = {14},
number = {4},
doi = {10.1016/0747-7171(92)90011-R},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/jsc92.pdf}
}
@inproceedings{miller92llworkshop,
author = {Dale Miller},
title = {Linear Logic and Logic Programming: An Overview},
booktitle = {Proceedings of the Workshop on Linear Logic and Logic
Programming (Washington, DC)},
editor = {Dale Miller},
month = nov,
year = {1992},
note = {Available as UPenn CIS technical report MS-CIS-92-80
and electronically from ftp.cis.upenn.edu in
pub/meetings/LL+LP-proceedings}
}
@inproceedings{miller92lpw,
author = {Dale Miller},
title = {A Proposal for Modules for {$\lambda$Prolog}:
Preliminary Draft},
booktitle = {Proceedings of the 1992 {$\lambda$Prolog Workshop}},
editor = {Dale Miller},
year = {1992}
}
@inproceedings{miller92rclp,
author = {Dale Miller},
title = {Abstract Syntax and Logic Programming},
booktitle = {{Logic Programming: Proceedings of the First Russian
Conference on Logic Programming, 14-18 September
1990}},
year = {1992},
pages = {322--337},
publisher = {Springer},
series = {LNAI},
number = {592}
}
@inproceedings{miller92welp,
author = {Dale Miller},
title = {The $\pi$-calculus as a theory in linear logic:
Preliminary results},
booktitle = {3rd Workshop on Extensions to Logic Programming},
editor = {E. Lamma and P. Mello},
publisher = {Springer},
address = {Bologna, Italy},
series = {LNCS},
number = {660},
pages = {242--265},
year = {1993},
doi = {10.1007/3-540-56454-3\_13}
}
@inproceedings{miller93welp,
author = {Dale Miller},
title = {A Proposal for Modules in {$\lambda$Prolog}},
booktitle = {4th Workshop on Extensions to Logic Programming},
editor = {R. Dyckhoff},
publisher = {Springer},
series = {LNCS},
number = {798},
pages = {206--221},
year = {1994}
}
@inproceedings{miller94lics,
author = {Dale Miller},
title = {A Multiple-Conclusion Meta-Logic},
booktitle = {9th Symp.\ on Logic in Computer Science},
editor = {S. Abramsky},
address = {Paris},
month = jul,
year = {1994},
publisher = {IEEE Computer Society},
pages = {272--281}
}
@article{miller95computnet,
author = {Dale Miller},
title = {A Survey of Linear Logic Programming},
journal = {Computational Logic: The Newsletter of the European
Network in Computational Logic},
volume = {2},
number = {2},
pages = {63--67},
year = {1995},
month = dec
}
@inproceedings{miller95gulp,
author = {Dale Miller},
title = {Observations about using logic as a specification
language},
booktitle = {Proceedings of GULP-PRODE'95: Joint Conference on
Declarative Programming},
editor = {M. Sessa},
address = {Marina di Vietri (Salerno-Italy)},
month = sep,
year = {1995}
}
@article{miller96tcs,
author = {Dale Miller},
title = {Forum: {A} Multiple-Conclusion Specification Logic},
journal = {Theoretical Computer Science},
year = {1996},
pages = {201--232},
volume = {165},
number = {1},
doi = {10.1016/0304-3975(96)00045-X}
}
@incollection{miller97nato,
author = {Dale Miller},
booktitle = {Logic of Computation},
title = {Logic Programming and Meta-Logic},
publisher = {Springer},
year = {1997},
editor = {Helmut Schwichtenberg},
volume = {157},
series = {Nato ASI Series},
pages = {265--308},
doi = {10.1007/978-3-642-58622-4\_11}
}
@unpublished{miller98lpbook,
author = {Dale Miller},
title = {{$\lambda$Prolog}: an introduction to the language and
its logic},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/bk.pdf},
year = {1998},
note = {Incomplete draft.}
}
@incollection{miller99nato,
author = {Dale Miller},
booktitle = {Computational Logic},
title = {Sequent Calculus and the Specification of
Computation},
publisher = {Springer},
year = {1999},
editor = {Ulrich Berger and Helmut Schwichtenberg},
volume = {165},
series = {Nato ASI Series},
pages = {399--444}
}
@article{miller99surveys,
author = {Dale Miller and Catuscia Palamidessi},
title = {Foundational Aspects of Syntax},
journal = {ACM Computing Surveys},
publisher = {ACM},
editor = {Pierpaolo Degano and Roberto Gorrieri and Alberto
Marchetti-Spaccamela and Peter Wegner},
year = {1999},
volume = {31},
month = sep,
doi = {10.1145/333580.333590}
}
@inproceedings{nadathur88iclp,
author = {Gopalan Nadathur and Dale Miller},
title = {An {Overview} of {$\lambda$Prolog}},
editor = {Kenneth A. Bowen and Robert A. Kowalski},
booktitle = {{Fifth International Logic Programming Conference}},
address = {Seattle},
publisher = {MIT Press},
pages = {810--827},
month = aug,
year = {1988},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/iclp88.pdf}
}
@article{nadathur90jacm,
author = {Gopalan Nadathur and Dale Miller},
title = {Higher-order {Horn} Clauses},
journal = {Journal of the ACM},
volume = {37},
number = {4},
month = oct,
year = {1990},
pages = {777--814},
doi = {10.1145/96559.96570}
}
@techreport{nadathur94tr,
author = {Gopalan Nadathur and Dale Miller},
title = {Higher-Order Logic Programming},
institution = {Department of Computer Science, Duke University},
year = {1994},
number = {CS-1994-38}
}
@incollection{nadathur98handbook,
author = {Gopalan Nadathur and Dale Miller},
booktitle = {{Handbook of Logic in Artificial Intelligence and
Logic Programming}},
title = {Higher-order Logic Programming},
publisher = {Clarendon Press, Oxford},
year = {1998},
editor = {Dov M. Gabbay and C. J. Hogger and J. A. Robinson},
volume = {5},
pages = {499--590}
}
@inproceedings{nigam08ijcar,
author = {Vivek Nigam and Dale Miller},
title = {Focusing in linear meta-logic},
booktitle = {Proceedings of IJCAR: International Joint Conference
on Automated Reasoning},
year = {2008},
editor = {Alessandro Armando and Peter Baumgartner and Gilles
Dowek},
url = {https://hal.inria.fr/inria-00281631/en/},
publisher = {Springer},
series = {LNAI},
pages = {507--522},
volume = {5195}
}
@unpublished{nigam08tr,
author = {Vivek Nigam and Dale Miller},
title = {Focusing in linear meta-logic: Extended Report},
url = {https://hal.inria.fr/inria-00281631},
year = {2008},
note = {Technical report}
}
@inproceedings{nigam09ppdp,
author = {Vivek Nigam and Dale Miller},
title = {Algorithmic specifications in linear logic with
subexponentials},
booktitle = {ACM SIGPLAN Conference on Principles and Practice of
Declarative Programming (PPDP)},
editor = {Ant\'onio Porto and Francisco Javier L\'opez-Fraguas},
pages = {129--140},
year = {2009},
publisher = {ACM},
doi = {10.1145/1599410.1599427}
}
@article{nigam10jar,
author = {Vivek Nigam and Dale Miller},
title = {A framework for proof systems},
volume = {45},
number = {2},
journal = {J. of Automated Reasoning},
pages = {157--188},
year = {2010},
url = {https://springerlink.com/content/m12014474287n423/},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/nigam-ijcar.pdf}
}
@inproceedings{pareschi90iclp,
title = {Extending Definite Clause Grammars with Scoping
Constructs},
author = {Remo Pareschi and Dale Miller},
year = {1990},
booktitle = {{1990 International Conference in Logic Programming}},
month = jun,
pages = {373--389},
publisher = {MIT Press},
editor = {David H. D. Warren and Peter Szeredi}
}
@inproceedings{pimentel05lpar,
author = {Elaine Pimentel and Dale Miller},
title = {On the specification of sequent systems},
booktitle = {LPAR 2005: 12th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning},
year = {2005},
pages = {352--366},
series = {LNAI},
number = {3835},
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lpar05.pdf}
}
@misc{tac.website,
title = {Tac: {A} Generic and Adaptable Interactive Theorem
Prover},
author = {David Baelde and Dale Miller and Zach Snow and
Alexandre Viel},
howpublished = {\url{https://slimmer.gforge.inria.fr/tac/}},
year = {2009},
key = {zzz}
}
@unpublished{taci,
author = {Zach Snow and David Baelde and Dale Miller},
title = {Taci: an interactive theorem proving framework},
year = {2007},
url = {https://gforge.inria.fr/projects/slimmer/},
note = {OCaml code.}
}
@inproceedings{tiu05eshol,
author = {Alwen Tiu and Gopalan Nadathur and Dale Miller},
title = {Mixing Finite Success and Finite Failure in an
Automated Prover},
booktitle = {Empirically Successful Automated Reasoning in
Higher-Order Logics (ESHOL'05)},
pages = {79--98},
year = {2005},
month = dec,
pdf = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/eshol05.pdf}
}
@inproceedings{tiu05fguc,
author = {Alwen Tiu and Dale Miller},
title = {A Proof Search Specification of the $\pi$-Calculus},
booktitle = {3rd Workshop on the Foundations of Global Ubiquitous
Computing},
year = {2005},
series = {ENTCS},
volume = {138},
pages = {79--101},
doi = {10.1016/j.entcs.2005.05.006},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fguc04workshop.pdf}
}
@article{tiu10tocl,
author = {Alwen Tiu and Dale Miller},
title = {Proof Search Specifications of Bisimulation and Modal
Logics for the $\pi$-calculus},
journal = {ACM Trans.\ on Computational Logic},
volume = {11},
number = {2},
pages = {13:1--13:35},
doi = {10.1145/1656242.1656248},
year = {2010}
}
@misc{trymlts.website,
author = {Ulysse G{\'e}rard and Dale Miller and Gabriel
Scherer},
title = {Try {MLTS} Online},
note = {\url{https://trymlts.github.io/}},
month = mar,
year = {2018}
}
@unpublished{viel10pstt,
author = {Alexandre Viel and Dale Miller},
title = {Proof search when equality is a logical connective},
note = {Unpublished draft presented to the International
Workshop on Proof-Search in Type Theories},
url = {https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/unif-equality.pdf},
month = jul,
year = {2010}
}
@inproceedings{ziegler05sos,
author = {Axelle Ziegler and Dale Miller and Catuscia
Palamidessi},
title = {A congruence format for name-passing calculi},
booktitle = {Structural Operational Semantics (SOS'05)},
month = jul,
year = {2005},
pages = {169--189},
series = {ENTCS},
address = {Lisbon, Portugal},
publisher = {Elsevier Science B.V.},
pdf = {https://www.lix.polytechnique.fr/parsifal/ziegler05report.pdf}
}
This file was generated by bibtex2html 1.99.