@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/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 = {Submitted to TCS},
year = {2012}
}
@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},
url = {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},
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}
}
@techreport{gazeau12hal,
hal_id = {hal-00665995},
institution = {INRIA},
url = {http://hal.inria.fr/hal-00665995},
title = {{A non-local method for robustness analysis of
floating point programs}},
author = {Ivan Gazeau and Dale Miller and Catuscia Palamidessi},
booktitle = {{QAPL - Tenth Workshop on Quantitative Aspects of
Programming Languages}},
address = {Tallinn, Estonie},
year = {2012},
month = feb,
note = {To appear in QAPL 2012.},
pdf = {http://hal.inria.fr/hal-00665995/PDF/proof\_example.pdf},
lixcategorie = {CIA},
lixequipe = {Parsifal}
}
@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},
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},
series = {LNCS},
number = {2556},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
month = dec,
pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fsttcs02.pdf},
dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fsttcs02.dvi}
}
@misc{miller02llw,
author = {Dale Miller},
title = {Higher-order quantification and proof search: an
extended abstract},
month = jul,
year = {2002},
note = {Presented at Linear Logic 2002, FLoC, Copenhagen},
lixequipe = {Parsifal},
x-pays = {},
lixcategorie = {AU}
}
@inproceedings{miller02tableaux,
author = {Dale Miller and Elaine Pimentel},
title = {Using linear logic to reason about sequent systems},
pages = {2--23},
editor = {Uwe Egly and Christian G. Ferm{\"u}ller},
booktitle = {International Conference on Automated Reasoning with
Analytic Tableaux and Related Methods},
publisher = {Springer},
series = {LNCS},
volume = {2381},
year = {2002},
dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tableaux02.dvi},
pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tableaux02.pdf},
lixequipe = {Parsifal},
x-pays = {BR},
lixcategorie = {CIA}
}
@inproceedings{miller03fcs,
author = {Dale Miller},
title = {Encryption as an Abstract Data-Type: An extended
abstract},
booktitle = {Proceedings of FCS'03: Foundations of Computer
Security},
editor = {Iliano Cervesato},
pages = {3--14},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
year = {2003},
dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fcs03.dvi},
pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fcs03.pdf},
ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/fcs03.ps}
}
@inproceedings{miller03lics,
author = {Dale Miller and Alwen Tiu},
title = {A Proof Theory for Generic Judgments: An extended
abstract},
booktitle = {18th Symp.\ on Logic in Computer Science},
pages = {118--127},
editor = {Phokion Kolaitis},
year = {2003},
month = jun,
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {AU},
publisher = {IEEE},
pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics03.pdf},
ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics03.ps},
dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics03.dvi}
}
@inproceedings{miller03tphols,
author = {Dale Miller},
title = {Reasoning about proof search specifications: An
abstract},
booktitle = {Theorem Proving in Higher Order Logics: 16th
International Conference, TPHOLs 2003},
pages = {204},
year = {2003},
volume = {2758},
series = {LNCS},
publisher = {Springer},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
note = {Invited speaker},
pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tphols03talk.pdf},
dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tphols03talk.dvi}
}
@inproceedings{miller03unif,
author = {Dale Miller},
title = {Definitions, Unification, and the Sequent Calculus},
booktitle = {Proceedings of the 17th International Workshop on
Unification, UNIF'03},
pages = {1--2},
year = {2003},
editor = {J. Levy and M. Kohlhase and J. Niehren and M.
Villaret},
series = {Technical Report DSIC-II/12/03},
month = jun,
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
organization = {Departamento de Sistemas Inform{\`a}tics i
Computaci{\'o} Universidad Polit{\`e}cnica de
Val{\`e}ncia},
note = {Invited talk}
}
@inproceedings{miller03wollic,
author = {Dale Miller},
title = {Encryption as an abstract data type},
booktitle = {WoLLIC'2003, 10th Workshop on Logic, Language,
Information and Computation},
series = {ENTCS},
volume = {84},
publisher = {Elsevier},
editor = {Ruy de Queiroz and Elaine Pimentel and Lucilia
Figueiredo},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {},
note = {Invited talk},
year = {2003}
}
@inproceedings{miller04csl,
author = {Dale Miller},
title = {Bindings, mobility of bindings, and the
$\nabla$-quantifier},
booktitle = {18th International Conference on Computer Science
Logic {(CSL)} 2004},
pages = {24},
year = {2004},
editor = {Jerzy Marcinkowski and Andrzej Tarlecki},
volume = {3210},
series = {LNCS},
pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/csl04talk.pdf},
lixcategorie = {CIA},
lixequipe = {Parsifal},
x-pays = {}
}
@incollection{miller04lc,
author = {Dale Miller and Elaine Pimentel},
title = {Linear logic as a framework for specifying sequent
calculus},
booktitle = {Logic Colloquium '99: Proceedings of the Annual
European Summer Meeting of the Association for Symbolic
Logic},
publisher = {A K Peters Ltd},
series = {Lecture Notes in Logic},
editor = {Jan van Eijck and Vincent van Oostrom and Albert
Visser},
pages = {111--135},
year = {2004},
pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lc99.pdf},
dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lc99.dvi},
ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lc99.ps},
lixcategorie = {OUV},
lixequipe = {Parsifal},
x-pays = {BR}
}
@incollection{miller04llcs,
author = {Dale Miller},
editor = {Thomas Ehrhard and Jean-Yves Girard and Paul Ruet and
Phil Scott},
booktitle = {Linear Logic in Computer Science},
title = {Overview of linear logic programming},
publisher = {Cambridge University Press},
series = {London Mathematical Society Lecture Note},
volume = {316},
year = {2004},
pages = {119--150},
ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.ps},
pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.pdf},
dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.dvi},
lixcategorie = {OUV},
lixequipe = {Parsifal},
x-pays = {}
}
@inproceedings{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},
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},
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},
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},
series = {LNAI},
number = {592}
}
@inproceedings{miller92welp,
author = {Dale Miller},
title = {The $\pi$-calculus as a theory in linear logic:
Preliminary results},
booktitle = {3rd Workshop on Extensions to Logic Programming},
editor = {E. Lamma and P. Mello},
publisher = {Springer},
address = {Bologna, Italy},
series = {LNCS},
number = {660},
pages = {242--265},
year = {1993},
url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/pic.pdf}
}
@inproceedings{miller93welp,
author = {Dale Miller},
title = {A Proposal for Modules in {$\lambda$Prolog}},
booktitle = {4th Workshop on Extensions to Logic Programming},
editor = {R. Dyckhoff},
publisher = {Springer},
series = {LNCS},
number = {798},
pages = {206--221},
year = {1994}
}
@inproceedings{miller94lics,
author = {Dale Miller},
title = {A Multiple-Conclusion Meta-Logic},
booktitle = {9th Symp.\ on Logic in Computer Science},
editor = {S. Abramsky},
address = {Paris},
month = jul,
year = {1994},
organization = {IEEE Computer Society Press},
pages = {272--281}
}
@article{miller95computnet,
author = {Dale Miller},
title = {A Survey of Linear Logic Programming},
journal = {Computational Logic: The Newsletter of the European
Network in Computational Logic},
volume = {2},
number = {2},
pages = {63--67},
year = {1995},
month = dec
}
@inproceedings{miller95gulp,
author = {Dale Miller},
title = {Observations about using logic as a specification
language},
booktitle = {Proceedings of GULP-PRODE'95: Joint Conference on
Declarative Programming},
editor = {M. Sessa},
address = {Marina di Vietri (Salerno-Italy)},
month = sep,
year = {1995}
}
@article{miller96tcs,
author = {Dale Miller},
title = {Forum: {A} Multiple-Conclusion Specification Logic},
journal = {Theoretical Computer Science},
year = {1996},
pages = {201--232},
month = sep,
volume = {165},
number = {1}
}
@incollection{miller97nato,
author = {Dale Miller},
booktitle = {Logic of Computation},
title = {Logic Programming and Meta-Logic},
publisher = {Springer},
year = {1997},
editor = {Helmut Schwichtenberg},
volume = {157},
series = {Nato ASI Series},
pages = {265--308}
}
@unpublished{miller98lpbook,
author = {Dale Miller},
title = {{$\lambda$Prolog}: an introduction to the language and
its logic},
url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/bk.pdf},
year = {1998},
note = {Incomplete draft.}
}
@incollection{miller99nato,
author = {Dale Miller},
booktitle = {Computational Logic},
title = {Sequent Calculus and the Specification of
Computation},
publisher = {Springer},
year = {1999},
editor = {Ulrich Berger and Helmut Schwichtenberg},
volume = {165},
series = {Nato ASI Series},
pages = {399--444}
}
@article{miller99surveys,
author = {Dale Miller and Catuscia Palamidessi},
title = {Foundational Aspects of Syntax},
journal = {ACM Computing Surveys},
publisher = {ACM},
editor = {Pierpaolo Degano and Roberto Gorrieri and Alberto
Marchetti-Spaccamela and Peter Wegner},
year = {1999},
volume = {31},
month = sep
}
@inproceedings{nadathur88iclp,
author = {Gopalan Nadathur and Dale Miller},
title = {An {Overview} of {$\lambda$Prolog}},
editors = {Kenneth A. Bowen and Robert A. Kowalski},
booktitle = {{Fifth International Logic Programming Conference}},
address = {Seattle},
publisher = {MIT Press},
pages = {810--827},
month = aug,
year = {1988},
url = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/iclp88.pdf}
}
@article{nadathur90jacm,
author = {Gopalan Nadathur and Dale Miller},
title = {Higher-order {Horn} Clauses},
journal = {Journal of the ACM},
volume = {37},
number = {4},
month = oct,
year = {1990},
pages = {777--814}
}
@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 was generated by bibtex2html 1.94.