miller.bib

@comment{{This file has been generated by bib2bib 1.97}}
@comment{{Command line: /usr/bin/bib2bib -ob miller.bib -c 'author : "\(Dale\|Dale A.\) Miller"' master.bib}}
@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},
  editors = {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 = {http://gforge.inria.fr/docman/view.php/367/705/userguide.pdf},
  year = {2006},
  lixcategorie = {AU},
  lixequipe = {Parsifal Slimmer},
  x-pays = {US,AU},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {diffusion}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/cade2007.pdf},
  doi = {10.1007/978-3-540-73595-3\_28},
  lixcategorie = {CIA},
  lixequipe = {Parsifal Slimmer},
  x-pays = {US,AU},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CADE},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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},
  keywords = {mobius, wp4},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lpar07final.pdf},
  doi = {10.1007/978-3-540-75560-9\_9},
  lixcategorie = {CIA},
  lixequipe = {Parsifal Slimmer},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LPAR}
}
@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 = {http://www.lix.polytechnique.fr/~dbaelde/productions/pool/mumall_draft_long.pdf},
  lixcategorie = {AU},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {rapport}
}
@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},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ijcar10.pdf},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {US},
  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 = {Journal of Formalized Reasoning},
  year = {2014},
  volume = {7},
  number = {2},
  doi = {10.6092/issn.1972-5787/4650},
  url = {http://jfr.unibo.it/article/download/4650/4137},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  x-pays = {US,SG},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-scientific-popularization = {yes}
}
@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},
  lixequipe = {Parsifal},
  lixcategorie = {OUV}
}
@inproceedings{blanco15iwil,
  author = {Roberto Blanco and Tomer Libal and Dale Miller},
  title = {Defining the meaning of {TPTP} formatted proofs},
  url = {http://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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{blanco15wof,
  author = {Roberto Blanco and Dale Miller},
  title = {Proof Outlines as Proof Certificates: a system
                 description},
  year = {2015},
  url = {http://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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@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},
  url = {https://doi.org/10.1007/978-3-319-63046-5_16},
  doi = {10.1007/978-3-319-63046-5_16},
  editor = {Leonardo de Moura},
  series = {Lecture Notes in Computer Science},
  volume = {10395},
  publisher = {Springer}
}
@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},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tcs08trackb.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {[B]},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {AT},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-pays = {US},
  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},
  pdf = {http://hal.inria.fr/hal-00937056/PDF/lkfexp.pdf},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  url = {http://hal.inria.fr/hal-00937056},
  x-id-hal = {hal-00937056},
  x-type = {article},
  x-support = {revue},
  x-pays = {AT}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  doi = {10.1007/978-3-642-38574-2\_11},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CADE},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CADE},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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},
  url = {http://dx.doi.org/10.1007/s10817-016-9380-6},
  doi = {10.1007/s10817-016-9380-6},
  note = {doi:\texttt{10.1007/s10817-016-9380-6}},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {AU},
  aeres = {Dummy Field},
  x-equipes = {Parsifal Slimmer},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {JAR}
}
@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},
  series = {ENTCS},
  number = {323},
  year = {2016},
  page = {93-108},
  doi = {10.1016/j.entcs.2016.06.007},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LFSA},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@misc{chihani16lprolog,
  author = {Zakaria Chihani and Dale Miller and Fabien Renaud},
  title = {Supporting $\lambda${Prolog} code},
  note = {\url{http://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},
  lixequipe = {Parsifal}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LICS},
  pages = {498--508},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics08b.pdf},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/apal-games.pdf},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {revue},
  lixcategorie = {RI},
  lixequipe = {Parsifal}
}
@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 = {http://plato.stanford.edu/archives/fall2006/entries/logic-linear/},
  year = {2006},
  lixcategorie = {OUV},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {diffusion}
}
@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},
  editors = {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}
}
@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},
  pages = {221--235},
  editor = {Mark Stickel},
  volume = {449},
  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 = {http://arxiv.org/pdf/0804.3914.pdf},
  doi = {10.1016/j.entcs.2008.12.118},
  lixcategorie = {CIA},
  lixequipe = {Parsifal Slimmer},
  x-pays = {US},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {[B]},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal Slimmer},
  x-pays = {US},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LICS},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics08a.pdf},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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 = {http://arxiv.org/abs/0908.1390},
  institution = {CoRR},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {rapport}
}
@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},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  x-pays = {US},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {revue},
  pdf = {http://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 = {http://arxiv.org/abs/0911.2993},
  doi = {10.1007/s10817-011-9218-1},
  journal = {J. of Automated Reasoning},
  volume = {49},
  number = {2},
  pages = {241--273},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  x-pays = {US}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/qapl-full-version.pdf}
}
@techreport{gazeau12hal,
  hal_id = {hal-00665995},
  institution = {INRIA},
  url = {http://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 = {http://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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {QAPL}
}
@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)},
  hal = {http://hal.inria.fr/hal-00780774},
  url = {http://rvg.web.cse.unsw.edu.au/eptcs/content.cgi?QAPL2013},
  year = {2013},
  pages = {1--18},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {QAPL},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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},
  lixcategorie = {RI},
  lixequipe = {Parsifal}
}
@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},
  lixequipe = {Parsifal},
  lixcategorie = {CIA}
}
@inproceedings{hannan88iclp,
  author = {John Hannan and Dale Miller},
  title = {Uses of higher-order unification for implementing
                 program transformers},
  editors = {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}
}
@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}
}
@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 = {http://repository.upenn.edu/cis_reports/695/}
}
@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 = {http://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}
}
@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}
}
@misc{heath.ptmc,
  author = {Quentin Heath and Dale Miller},
  title = {A proof theory for model checking},
  month = apr,
  year = {2016},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ptmc-draft.pdf}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/pxtp2015.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CADE},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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},
  lixequipe = {Parsifal}
}
@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}
}
@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}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {US,GB},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {GPCE}
}
@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},
  keywords = {mobius, wp4},
  year = {2007},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/csl07liang.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {US},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CSL}
}
@unpublished{liang07report,
  author = {Chuck Liang and Dale Miller},
  title = {On focusing and polarities in linear logic and
                 intuitionistic logic},
  url = {http://hal.inria.fr/inria-00167231/},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/focusli.pdf},
  month = sep,
  year = {2007},
  lixcategorie = {AU},
  lixequipe = {Parsifal},
  x-pays = {US},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {rapport},
  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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {US},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LICS},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/liang09lics.pdf},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  x-pays = {US},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {TCS},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  doi = {10.1016/j.tcs.2009.07.041}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lku.pdf},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  x-pays = {US},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {APAL},
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@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 = {http://hal.inria.fr/hal-00787601},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {revue}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {US},
  aeres = {Dummy Field},
  hal = {http://hal.inria.fr/hal-00906299},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics13.pdf},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LICS},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/subdelimlncs.pdf},
  number = {9450},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@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},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mcdowell01.pdf},
  lixequipe = {Parsifal Slimmer},
  x-pays = {US},
  lixcategorie = {RI}
}
@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},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  x-pays = {US},
  pages = {411--437},
  dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tcs97.dvi},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tcs97.pdf},
  ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tcs97.ps}
}
@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.fac,
  author = {Dale Miller},
  title = {Proof Checking and Logic Programming},
  journal = {Formal Aspects of Computing},
  year = {2016},
  doi = {10.1007/s00165-016-0393-z},
  note = {To appear.}
}
@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 = {http://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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  series = {LNCS},
  pdf = {http://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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  month = dec,
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fsttcs02.pdf},
  dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fsttcs02.dvi}
}
@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},
  lixequipe = {Parsifal},
  x-pays = {},
  lixcategorie = {AU}
}
@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},
  dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tableaux02.dvi},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tableaux02.pdf},
  lixequipe = {Parsifal},
  x-pays = {BR},
  lixcategorie = {CIA}
}
@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 = {3--14},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  year = {2003},
  dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fcs03.dvi},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fcs03.pdf},
  ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fcs03.ps}
}
@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,
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {AU},
  publisher = {IEEE},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics03.pdf},
  ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics03.ps},
  dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics03.dvi}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  note = {Invited speaker},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tphols03talk.pdf},
  dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tphols03talk.dvi}
}
@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,
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/csl04talk.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {}
}
@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},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lc99.pdf},
  dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lc99.dvi},
  ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lc99.ps},
  lixcategorie = {OUV},
  lixequipe = {Parsifal},
  x-pays = {BR}
}
@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},
  ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.ps},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.pdf},
  dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.dvi},
  lixcategorie = {OUV},
  lixequipe = {Parsifal},
  x-pays = {}
}
@inproceedings{miller05apc,
  author = {Dale Miller},
  title = {Algebraic Process Calculi: The First Twenty Five Years
                 and Beyond},
  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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {AU},
  aeres = {Dummy Field},
  x-equipes = {Parsifal Slimmer},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {TOCL},
  pages = {749--783},
  publisher = {ACM Press},
  address = {New York, NY, USA},
  year = {2005},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tocl-nabla.pdf}
}
@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 = {http://www.cs.kuleuven.ac.be/~dtai/projects/ALP/newsletter/feb06/nav/articles/Dale/dale.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {diffusion}
}
@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},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ijcar06.pdf},
  dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ijcar06.dvi},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {IJCAR}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {[B]},
  pdf = {http://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},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ppdp06.pdf},
  ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ppdp06.ps},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {PPDP}
}
@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},
  keywords = {mobius, wp4},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/csl07nigam.pdf},
  doi = {10.1007/978-3-540-74915-8\_35},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CSL}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/csl07saurin.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CSL}
}
@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},
  editors = {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},
  lixcategorie = {OUV},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  pdf = {http://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 = {http://www.ru.is/faculty/luca/BEATCS/miller.pdf},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes}
}
@unpublished{miller08unp,
  author = {Dale Miller and Vivek Nigam},
  title = {Proofs with tables},
  note = {Available via the authors web pages},
  year = {2008},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {rapport}
}
@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},
  lixcategorie = {Cinv},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/aplas10.pdf},
  lixcategorie = {Cinv},
  lixequipe = {Parsifal Slimmer},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {APLAS},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {yes},
  x-scientific-popularization = {no}
}
@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},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-pays = {UK},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  url = {http://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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CPP},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no},
  url = {http://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 = {http://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},
  lixcategorie = {OUV},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {livre},
  x-editorial-board = {no},
  x-proceedings = {no},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {yes}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/cpp2013.pdf},
  hal = {http://hal.inria.fr/hal-00863561/},
  address = {Melburne, Australia},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lfmtp13.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-international-audience = {yes},
  x-proceedings = {yes},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {yes},
  x-scientific-popularization = {no}
}
@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},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  url = {http://hal.inria.fr/hal-00787586}
}
@techreport{miller13tr,
  author = {Dale Miller and Alwen Tiu},
  title = {Extracting Proofs from Tabled Proof Search: Extended
                 version},
  institution = {INRIA-HAL},
  year = {2013},
  url = {http://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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/appa2014.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@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,
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@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},
  url = {http://dx.doi.org/10.1007/s00165-016-0393-z},
  pdf = {https://hal.inria.fr/hal-01390901/file/paper.pdf},
  hal_id = {hal-01390901},
  hal_version = {v1},
  lixcategorie = {RI},
  lixequipe = {Parsifal}
}
@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}
}
@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},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@phdthesis{miller83,
  author = {Dale A. Miller},
  title = {Proofs in Higher-order Logic},
  school = {Carnegie-Mellon University},
  month = aug,
  year = {1983},
  url = {http://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 A. 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},
  editors = {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}
}
@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},
  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}
}
@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 = {http://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 = {http://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},
  editors = {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 = {http://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}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/AbsInLP.pdf.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 = {Informal Proceedings of the Logical Frameworks BRA
                 Workshop},
  address = {Nice, France},
  note = {Available as UPenn CIS technical report MS-CIS-90-59},
  url = {http://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,
  note = {Guest editorial.},
  url = {http://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},
  pages = {125--157}
}
@inproceedings{miller91elp,
  author = {Dale Miller},
  editor = {Peter Schroeder-Heister},
  title = {A Logic Programming Language with Lambda-Abstraction,
                 Function Variables, and Simple Unification},
  booktitle = {{Extensions of Logic Programming: International
                 Workshop, T\"ubingen}},
  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},
  editors = {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}
}
@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},
  pdf = {http://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},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/pic.pdf}
}
@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},
  organization = {IEEE Computer Society Press},
  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},
  month = sep,
  volume = {165},
  number = {1}
}
@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}
}
@unpublished{miller98lpbook,
  author = {Dale Miller},
  title = {{$\lambda$Prolog}: an introduction to the language and
                 its logic},
  url = {http://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
}
@inproceedings{nadathur88iclp,
  author = {Gopalan Nadathur and Dale Miller},
  title = {An {Overview} of {$\lambda$Prolog}},
  editors = {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 = {http://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}
}
@techreport{nadathur94tr,
  author = {Gopalan Nadathur and Dale Miller},
  title = {Higher-Order Logic Programming},
  institution = {Department of Computer Science, Duke University},
  year = {1994},
  type = {Technical Report},
  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},
  editors = {Alessandro Armando and Peter Baumgartner and Gilles
                 Dowek},
  url = {http://hal.inria.fr/inria-00281631/en/},
  publisher = {Springer},
  series = {LNAI},
  pages = {507--522},
  volume = {5195},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  keywords = {mobius, wp4},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {IJCAR},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@unpublished{nigam08tr,
  author = {Vivek Nigam and Dale Miller},
  title = {Focusing in linear meta-logic: Extended Report},
  url = {http://hal.inria.fr/inria-00281631},
  year = {2008},
  note = {Technical report},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {rapport}
}
@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)},
  editors = {Ant\'onio Porto and Francisco Javier L\'opez-Fraguas},
  pages = {129--140},
  year = {2009},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {PPDP},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ppdp09.pdf},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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 = {http://springerlink.com/content/m12014474287n423/},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/nigam-ijcar.pdf},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  x-pays = {US},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {revue}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lpar05.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {BR},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LPAR},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@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{http://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 = {http://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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/eshol05.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal Slimmer},
  x-pays = {US,AU},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes}
}
@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 = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fguc04workshop.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {}
}
@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},
  doi = {10.1145/1656242.1656248},
  url = {http://arxiv.org/abs/0805.2785},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {revue},
  lixcategorie = {RI},
  lixequipe = {Parsifal},
  x-pays = {AU},
  year = {2010}
}
@unpublished{viel10pstt,
  author = {Alexandre Viel and Dale Miller},
  title = {Proof search when equality is a logical connective},
  note = {Presented to the International Workshop on
                 Proof-Search in Type Theories},
  url = {http://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 = {http://www.lix.polytechnique.fr/parsifal/ziegler05report.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  x-pays = {},
  aeres = {Dummy Field},
  x-equipes = {parsifal comete},
  x-type = {article},
  x-support = {actes}
}

This file was generated by bibtex2html 1.97.