miller.bib

@COMMENT{{{This file has been generated by bib2bib 1.73}}
@COMMENT{{{Command line: bib2bib -ob miller.bib -c 'author : "\(Dale\|Dale A.\) Miller"' master.bib}}
@UNPUBLISHED{gacek.twolevel,
  AUTHOR = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  TITLE = {A two-level logic approach to reasoning about
                 computations},
  YEAR = {2010},
  MONTH = AUG,
  URL = {http://arxiv.org/abs/0911.2993},
  NOTE = {Accepted to the J. of Automated Reasoning},
  LIXCATEGORIE = {AU},
  LIXEQUIPE = {Parsifal},
  X-PAYS = {US}
}
@UNPUBLISHED{liang.pil,
  AUTHOR = {Chuck Liang and Dale Miller},
  TITLE = {Kripke Semantics and Proof Systems for Combining
                 Intuitionistic Logic and Classical Logic},
  NOTE = {Submitted},
  MONTH = SEP,
  YEAR = {2011}
}
@UNPUBLISHED{miller.cppa,
  AUTHOR = {Dale Miller},
  TITLE = {Communicating and trusting proofs: The case for broad
                 spectrum proof certificates},
  NOTE = {Available from author's website},
  MONTH = JUN,
  YEAR = {2011},
  X-EDITORIAL-BOARD = {no},
  X-PROCEEDINGS = {no},
  X-INTERNATIONAL-AUDIENCE = {no}
}
@UNPUBLISHED{miller.tcs,
  AUTHOR = {Dale Miller and Elaine Pimentel},
  TITLE = {A formal framework for specifying sequent calculus
                 proof systems},
  NOTE = {35 page draft to be submitted},
  YEAR = {2011}
}
@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}
}
@UNPUBLISHED{nigam08tr,
  AUTHOR = {Vivek Nigam and Dale Miller},
  TITLE = {Focusing in linear meta-logic: Extended Report},
  NOTE = {Available from http://hal.inria.fr/inria-00281631},
  YEAR = {2008},
  AERES = {Dummy Field},
  X-EQUIPES = {parsifal},
  X-TYPE = {article},
  X-SUPPORT = {rapport}
}
@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}
}
@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}
}
@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},
  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},
  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}
}
@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{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},
  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},
  URL = {http://dx.doi.org/10.1016/j.apal.2009.07.017},
  PDF = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/game08draft.pdf},
  AERES = {Dummy Field},
  X-EQUIPES = {parsifal},
  X-TYPE = {article},
  X-SUPPORT = {revue},
  LIXCATEGORIE = {AU},
  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-Verlag},
  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},
  URL = {http://dx.doi.org/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},
  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}
}
@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 = {H. Abramson and M. Rogers},
  PUBLISHER = {{MIT} Press},
  PAGES = {453--476},
  YEAR = {1989}
}
@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-Verlag},
  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}
}
@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 = {CIA},
  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},
  URL = {http://dx.doi.org/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 = {http://dx.doi.org/10.1016/j.apal.2011.01.012},
  URL = {http://dx.doi.org/10.1016/j.apal.2011.01.012},
  PDF = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lku.pdf},
  LIXCATEGORIE = {CIA},
  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{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}
}
@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.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/ltrees.pdf}
}
@INPROCEEDINGS{miller01entcs,
  AUTHOR = {Dale Miller},
  TITLE = {Encoding Generic Judgments: Preliminary results},
  BOOKTITLE = {ENTCS},
  VOLUME = {58},
  NUMBER = {1},
  PUBLISHER = {Elsevier Science Publishers},
  EDITOR = {R. L. Crole S. J. Ambler and A. Momigliano},
  NOTE = {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-Verlag},
  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-Verlag},
  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{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},
  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},
  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},
  X-PAYS = {},
  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 = {OUV},
  LIXEQUIPE = {Parsifal},
  X-PAYS = {},
  AERES = {Dummy Field},
  X-EQUIPES = {parsifal},
  X-TYPE = {article},
  X-SUPPORT = {actes}
}
@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,
  URL = {http://dx.doi.org/10.1016/j.entcs.2009.07.020},
  LIXCATEGORIE = {OUV},
  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 = {CIA},
  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 = {ACM-BCS-Visions Conference},
  MONTH = APR,
  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},
  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}
}
@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-Verlag},
  YEAR = {1982},
  EDITOR = {Donald W. Loveland},
  SERIES = {LNCS},
  VOLUME = {138},
  PAGES = {50--69}
}
@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-Verlag},
  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}
}
@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-Verlag},
  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}
}
@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 and
                 Second Russian Conferences on Logic Programming}},
  YEAR = {1992},
  PAGES = {322--337},
  PUBLISHER = {Springer-Verlag},
  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-Verlag},
  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-Verlag},
  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}
}
@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},
  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}
}
@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)},
  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}
}
@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}
}
@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{tiu04fguc,
  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},
  MONTH = SEP,
  YEAR = {2004},
  SERIES = {ENTCS},
  VOLUME = {138},
  PAGES = {79--101},
  PDF = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fguc04workshop.pdf},
  LIXCATEGORIE = {CIA},
  LIXEQUIPE = {Parsifal},
  X-PAYS = {}
}
@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}
}
@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},
  URL = {http://arxiv.org/abs/0805.2785},
  AERES = {Dummy Field},
  X-EQUIPES = {parsifal EXT},
  X-TYPE = {article},
  X-SUPPORT = {revue},
  LIXCATEGORIE = {CIA},
  LIXEQUIPE = {Parsifal},
  X-PAYS = {AU},
  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 has been generated by bibtex2html 1.73