miller.bib

@COMMENT{{This file has been generated by bib2bib 1.88}}
@COMMENT{{Command line: /usr/bin/bib2bib -ob /home/dale/www/papers/miller.bib -c 'author : "\(Dale\|Dale A.\) Miller"' /home/dale/pap/references/master.bib}}
@UNPUBLISHED{delande08unp,
  author = {Olivier Delande and Dale Miller and Alexis Saurin},
  title = {Proof and refutation in {MALL} as a game},
  note = {Submitted for publication},
  month = OCT,
  year = {2008},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {???},
  lixcategorie = {AU},
  lixequipe = {Parsifal}
}
@UNPUBLISHED{miller08unp,
  author = {Dale Miller and Vivek Nigam},
  title = {Proofs with tables},
  note = {Available via the authors web pages},
  year = {2008},
  note = {Preprint},
  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}
}
@UNPUBLISHED{tiu.tocl,
  author = {Alwen Tiu and Dale Miller},
  title = {Proof Search Specifications of Bisimulation and Modal
                 Logic for the $\pi$-calculus},
  note = {Submitted May 2008.},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {???},
  lixcategorie = {AU},
  lixequipe = {Parsifal},
  year = {2008}
}
@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},
  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 Conference on Automated Deduction (CADE)},
  pages = {391--397},
  year = {2007},
  editor = {Frank Pfenning},
  number = {4603},
  series = {LNAI},
  publisher = {Springer},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/cade2007.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  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},
  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},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {rapport}
}
@INPROCEEDINGS{chaudhuri08tcs,
  author = {Kaustuv Chaudhuri and Dale Miller and Alexis Saurin},
  title = {Canonical Sequent Proofs via Multi-Focusing},
  booktitle = {Fifth IFIP International Conference on Theoretical
                 Computer Science},
  publisher = {Boston: Springer},
  year = {2008},
  volume = {273},
  series = {IFIP International Federation for Information
                 Processing},
  editor = {Giorgio Ausiello and Juhani Karhum{\"a}ki and
                 Giancarlo Mauri and Luke Ong},
  month = SEP,
  pages = {383--396},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {[B]},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tcs08trackb.pdf},
  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},
  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}
}
@INCOLLECTION{dicosmo06sep,
  author = {Roberto DiCosmo 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},
  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}
}
@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 = {LFMTP 2008: International Workshop on Logical
                 Frameworks and Meta-Languages: Theory and Practice},
  year = {2008},
  editor = {A. Abel and C. Urban},
  pages = {75--89},
  pdf = {http://arxiv.org/pdf/0804.3914.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  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},
  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}
}
@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 International Conference 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},
  note = {UPenn CIS Tech Report MS-CIS-89-28}
}
@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 = {{Sixth Annual Symposium 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, {\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},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {GPCE}
}
@UNPUBLISHED{liang.tcs,
  author = {Chuck Liang and Dale Miller},
  title = {Focusing and Polarization in Linear, Intuitionistic,
                 and Classical Logics},
  year = {2008},
  note = {Accepted to {\em Theoretical Computer Science}}
}
@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},
  note = {Extended version to appear in TCS.},
  keywords = {mobius, wp4},
  year = {2007},
  url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/csl07liang.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  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},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {rapport}
}
@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},
  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},
  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 = {Electronic Notes in Theoretical Computer Science},
  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{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.}
}
@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 = {Computational Logic - {CL} 2000},
  pages = {239--253},
  year = {2000},
  editor = {John Lloyd and {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},
  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},
  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},
  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},
  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},
  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},
  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},
  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},
  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 = {Electronic Notes in Theoretical Computer Science},
  volume = {84},
  publisher = {Elsevier},
  editor = {Ruy de Queiroz and Elaine Pimentel and Lucilia
                 Figueiredo},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  note = {Invited talk},
  year = {2003}
}
@INPROCEEDINGS{miller04csl,
  author = {Dale Miller},
  title = {Bindings, mobility of bindings, and the
                 $\nabla$-quantifier},
  booktitle = {18th International Workshop {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}
}
@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}
}
@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}
}
@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},
  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},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {TOCL},
  pages = {749--783},
  publisher = {ACM Press},
  address = {New York, NY, USA},
  year = {2005},
  pdf = {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},
  pdf = {http://www.cs.kuleuven.ac.be/~dtai/projects/ALP/newsletter/feb06/nav/articles/Dale/dale.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  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},
  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 = {Electr. Notes Theor. Comput. Sci},
  year = {2006},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  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},
  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},
  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 = {Festschrift for Peter Andrews},
  publisher = {Elsevier},
  year = {2008},
  series = {Studies in Logic},
  note = {To appear.},
  lixcategorie = {OUV},
  lixequipe = {Parsifal},
  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},
  aeres = {Dummy Field},
  x-equipes = {parsifal},
  x-type = {article},
  x-support = {actes}
}
@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 = {Symposium 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 A. 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 = {Ninth {Annual Symposium 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}
}
@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},
  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{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},
  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/}
}
@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}
}
@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},
  aeres = {Dummy Field},
  x-equipes = {parsifal EXT},
  x-type = {article},
  x-support = {actes}
}
@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 = {Electronic Notes in Theoretical Computer Science},
  address = {Lisbon, Portugal},
  publisher = {Elsevier Science B.V.},
  pdf = {http://www.lix.polytechnique.fr/parsifal/ziegler05report.pdf},
  lixcategorie = {CIA},
  lixequipe = {Parsifal},
  aeres = {Dummy Field},
  x-equipes = {parsifal comete},
  x-type = {article},
  x-support = {actes}
}

This file has been generated by bibtex2html 1.88.