urbain.bib

@comment{{This file has been generated by bib2bib 1.98}}

@comment{{Command line: /usr/bin/bib2bib -q -oc urbain.cite -ob urbain.bib -c 'author : "urbain"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}

@inproceedings{marche98rta,
  author = {Claude March{\'e} and Xavier Urbain},
  title = {Termination of Associative-Commutative Rewriting by Dependency Pairs},
  crossref = {rta98},
  year = 1998,
  pages = {241--255},
  x-pdf = {http://www.lri.fr/~marche/articles/rta98.ps.gz},
  abstract = {http://www.lri.fr/~marche/rta98.html},
  type_publi = {icolcomlec},
  topics = {team, lri, cclserver},
  clef_labo = {MU98E}
}

@mastersthesis{urbain96,
  author = {Xavier Urbain},
  title = {Interpr{\'e}tations polynomiales et applications aux
  $\lambda$-calculs avec substitutions explicites},
  school = {Universit{\'e} Paris-sud},
  year = 1996,
  type = {Rapport de stage de Ma{\^\i}trise},
  x-pdf = {http://www.lri.fr/~marche/articles/urbain.ps.gz},
  abstract = {http://www.lri.fr/~marche/urbain.html},
  type_publi = {?},
  topics = {team},
  location = {CM}
}

@mastersthesis{urbain97dea,
  author = {Xavier Urbain},
  title = {Preuves de terminaison {\`a} l'aide de paires de
d{\'e}pendances},
  school = {Universit{\'e} Paris-Sud},
  year = 1997,
  address = {Orsay, France},
  type = {Rapport de {DEA}},
  topics = {team}
}

@unpublished{duran_sub,
  author = {Francisco Duran and Salvador Lucas and
  Claude {March\'e} and {Jos\'e} Meseguer and Xavier Urbain},
  title = {Termination of Membership Equational Programs},
  note = {Submitted}
}

@inproceedings{gutierrez08rta,
  author = {Ra{\'u}l Guti{\'e}rrez and
               Salvador Lucas and
               Xavier Urbain},
  title = {Usable Rules for Context-Sensitive Rewrite Systems},
  booktitle = {rta08},
  year = {2008},
  pages = {126-141},
  ee = {http://dx.doi.org/10.1007/978-3-540-70590-1_9},
  crossref = {rta08}
}

@inproceedings{courtieu08tphols,
  author = {Pierre Courtieu and Julien Forest and Xavier Urbain},
  title = {Certifying a {T}ermination {C}riterion {B}ased on {G}raphs, {W}ithout {G}raphs},
  crossref = {tphols2008},
  pages = {183--198},
  type_publi = {icolcomlec}
}

@techreport{catano03deliv,
  author = {N\'estor Cata{\~n}o and Marek Gawkowski and
Marieke Huisman and Bart Jacobs and Claude March{\'e} and Christine Paulin
and Erik Poll and Nicole Rauch and Xavier Urbain},
  title = {Logical Techniques for Applet Verification},
  institution = {IST VerifiCard Project},
  year = 2003,
  type = {Deliverable},
  number = {5.2},
  note = {\url{http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf}},
  url = {http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf},
  topics = {team}
}

@misc{cime2,
  author = {Evelyne Contejean and Claude March{\'e} and
                  Benjamin Monate and Xavier Urbain},
  title = {{CiME version 2}},
  note = {Available at
                  \url{http://cime.lri.fr/}},
  year = 2000,
  url = {http://cime.lri.fr/},
  topics = {team,lri}
}

@techreport{kmu2002rr,
  author = {Keiichirou Kusakari and Claude March\'e and Xavier Urbain},
  title = {Termination of Associative-Commutative Rewriting using Dependency Pairs Criteria},
  institution = {LRI},
  year = 2002,
  type = {Research Report},
  number = 1304,
  type_publi = {interne},
  topics = {team},
  note = {\url{http://www.lri.fr/~urbain/textes/rr1304.ps.gz}},
  url = {http://www.lri.fr/~urbain/textes/rr1304.ps.gz}
}

@misc{krakatoa,
  author = {Jean-Christophe Filli{\^a}tre and Claude March\'e and Christine Paulin and Xavier Urbain},
  title = {The \textsc{Krakatoa} proof tool},
  year = 2003,
  note = {\url{http://krakatoa.lri.fr/}}
}

@misc{krakatoa02,
  author = {Claude March\'e and Christine Paulin and Xavier Urbain},
  title = {The \textsc{Krakatoa} proof tool},
  year = 2002,
  note = {\url{http://krakatoa.lri.fr/}}
}

@inproceedings{contejean03wst,
  author = {\'Evelyne Contejean and Claude March{\'e} and Benjamin Monate and Xavier Urbain},
  title = {Proving Termination of Rewriting with {\sc C\textit{i}ME}},
  crossref = {wst03},
  pages = {71--73},
  year = 2003,
  topics = {team},
  type_publi = {icolcomlec},
  url = {http://cime.lri.fr}
}

@techreport{contejean04rr,
  author = {\'Evelyne Contejean and Claude March{\'e} and Ana-Paula Tom{\'a}s and Xavier Urbain},
  title = {Mechanically proving termination using polynomial interpretations},
  institution = {LRI},
  year = {2004},
  type = {Research Report},
  number = {1382},
  type_publi = {interne},
  topics = {team},
  url = {http://www.lri.fr/~urbain/textes/rr1382.ps.gz}
}

@article{contejean05jar,
  author = {\'Evelyne Contejean and Claude March{\'e} and Ana Paula Tom{\'a}s and Xavier Urbain},
  title = {Mechanically proving termination using polynomial
   interpretations},
  journal = {Journal of Automated Reasoning},
  volume = {34},
  number = {4},
  pages = {325--363},
  year = 2005,
  type_publi = {irevcomlec},
  topics = {team},
  doi = {10.1007/s10817-005-9022-x},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {JAR},
  abstract = {http://www.lri.fr/~contejea/publis/2005jar/abstract.html}
}

@inproceedings{contejean07frocos,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
  title = {Certification of automated termination proofs},
  crossref = {frocos07},
  pages = {148--162},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {FROCOS},
  topics = {team},
  doi = {10.1007/978-3-540-74621-8_10},
  abstract = {http://www.lri.fr/~contejea/publis/2007frocos/abstract.html}
}

@inproceedings{contejean08wsct,
  author = {\'Evelyne Contejean and Xavier Urbain},
  title = {{The A3PAT approach}},
  booktitle = { Workshop on Certified Termination WScT08},
  year = 2008,
  address = {Leipzig, Germany},
  month = may,
  topics = {team},
  x-international-audience = {yes},
  x-proceedings = {no}
}

@misc{cime3,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
  title = {{CiME3}},
  year = 2007,
  url = {{http://cime.lri.fr}},
  note = {\url{http://cime.lri.fr}},
  topics = {team,lri},
  type_publi = {autre},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}

@inproceedings{contejean10pepm,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and  Andrei Paskevich and Olivier Pons and Xavier Urbain},
  title = {{A3PAT, an Approach for Certified Automated Termination Proofs}},
  crossref = {pepm10},
  booktitle = {Partial Evaluation and Program Manipulation},
  year = 2010,
  month = jan,
  pages = {63-72},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {PEPM},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  topics = {team},
  doi = {10.1145/1706356.1706370},
  abstract = {http://www.lri.fr/~contejea/publis/2010pepm/abstract.html}
}

@inproceedings{contejean11rta,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest
                  and Olivier Pons and Xavier Urbain},
  crossref = {rta11},
  title = {{Automated Certified Proofs with CiME3}},
  x-equipes = {demons PROVAL ext},
  url = {http://drops.dagstuhl.de/opus/volltexte/2011/3119},
  hal = {http://hal.inria.fr/hal-00777669},
  urn = {urn:nbn:de:0030-drops-31192},
  doi = {10.4230/LIPIcs.RTA.2011.21},
  pages = {21--30},
  abstract = {http://www.lri.fr/~contejea/publis/2011rta/abstract.html},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {RTA},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  topics = {team}
}

@techreport{contejean07rr,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
  title = {Certification of automated termination proofs},
  institution = {CEDRIC},
  year = 2007,
  type = {Research Report},
  number = 1185,
  month = {May},
  topics = {team},
  type_digiteo = {no},
  type_publi = {interne},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {rapport}
}

@unpublished{contejean99,
  author = {\'Evelyne Contejean and Claude March{\'e} and
                  Ana-Paola Tom{\'a}s and Xavier Urbain},
  title = {Solving Termination Constraints via finite domain polynomial
                   interpretations},
  note = {Unpublished draft, International Workshop on
                  Constraints in Computational Logics, Gif-sur-Yvette,
                  France},
  year = 1999,
  month = sep
}

@inproceedings{duran04pepm,
  author = {Francisco Dur{\'a}n and Salvador Lucas and Jos{\'e} Meseguer
and Claude March{\'e} and Xavier  Urbain},
  title = {Proving Termination of Membership Equational Programs},
  crossref = {pepm04},
  topics = {team},
  type_publi = {icolcomlec}
}

@article{duran06hosc,
  author = {Francisco Dur{\'a}n and Salvador Lucas and Jos{\'e} Meseguer
and Claude March{\'e} and Xavier  Urbain},
  title = {Proving Operational Termination of Membership Equational Programs},
  journal = {Higher-Order and Symbolic Computation},
  year = 2008,
  type_publi = {irevcomlec},
  type_digiteo = {revue_cl},
  topics = {team},
  volume = 21,
  number = {1--2},
  pages = {59--88},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {revue},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-cle-support = {HSC},
  x-pdf = {http://www.lri.fr/~marche/duran08hosc.pdf},
  hal = {http://hal.inria.fr/inria-00431474/en/},
  url = {http://www.lri.fr/~marche/duran08hosc.pdf}
}

@article{marche2004jsc,
  author = {Claude March\'e and Xavier Urbain},
  title = {Modular and Incremental Proofs of {AC}-Termination},
  journal = {Journal of Symbolic Computation},
  volume = 38,
  pages = {873--897},
  year = 2004,
  topics = {team},
  type_digiteo = {revue_cl},
  type_publi = {irevcomlec},
  url = {http://authors.elsevier.com/sd/article/S074771710400029X}
}

@article{marche04jlap,
  author = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain},
  title = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}},
  journal = {Journal of Logic and Algebraic Programming},
  year = 2004,
  volume = 58,
  number = {1--2},
  pages = {89--106},
  note = {\url{http://krakatoa.lri.fr}},
  url = {http://krakatoa.lri.fr},
  ps = {http://www.lri.fr/~marche/marche04jlap.ps},
  topics = {team},
  type_publi = {irevcomlec}
}

@inproceedings{urbain01ijcar,
  author = {Xavier Urbain},
  title = {Automated Incremental Termination Proofs for Hierarchically
                  defined Term Rewriting Systems},
  crossref = {ijcar01},
  pages = {485--498},
  year = 2001,
  topics = {team, rewriting, lri},
  type_publi = {icolcomlec},
  url = {http://www.lri.fr/~urbain/textes/ijcar01.ps.gz}
}

@phdthesis{urbain01these,
  author = {Xavier Urbain},
  topics = {team, lri},
  title = {Approche incr{\'e}mentale des preuves automatiques de
                   terminaison},
  school = {Universit{\'e} Paris-Sud},
  year = 2001,
  type = {Th{\`e}se de Doctorat},
  address = {Orsay, France},
  month = oct,
  type_publi = {these},
  note = {\url{http://www.lri.fr/~urbain/textes/these.ps.gz}},
  url = {http://www.lri.fr/~urbain/textes/these.ps.gz}
}

@article{urbain04jar,
  author = {Xavier Urbain},
  title = {Modular and Incremental Automated Termination Proofs},
  journal = {Journal of Automated Reasoning},
  year = {2004},
  volume = 32,
  pages = {315--355},
  topics = {team},
  type_publi = {irevcomlec},
  url = {http://www.lri.fr/~urbain/textes/jar.ps.gz}
}

@techreport{urbain2002rr,
  author = {Xavier Urbain},
  title = {Modular {\&} Incremental Proofs of {AC}-Termination},
  institution = {LRI},
  year = {2002},
  type = {Research Report},
  number = {1317},
  type_publi = {interne},
  topics = {team},
  url = {http://www.lri.fr/~urbain/textes/rr1317.ps.gz}
}

@techreport{urbain2002rr2,
  author = {Xavier Urbain},
  title = {Modular {\&} Incremental Automated Termination Proofs},
  institution = {LRI},
  year = {2002},
  type = {Research Report},
  number = {1326},
  type_publi = {interne},
  topics = {team},
  url = {http://www.lri.fr/~urbain/textes/rr1326.ps.gz}
}

@techreport{verificard52,
  author = {N{\'e}stor {Cata{\~n}o} and M. Gawlowski and Marieke Huisman and Bart Jacobs and Claude March\'e and Christine Paulin and Erik Poll and Nicole Rauch and Xavier Urbain},
  title = {Logical Techniques for Applet Verification},
  institution = {IST VerifiCard project},
  year = 2003,
  type = {Deliverable},
  number = {5.2},
  topics = {team},
  type_publi = {rapport}
}

@phdthesis{urbain10hdr,
  author = {Xavier Urbain},
  title = {Preuve automatique : techniques, outils et certification},
  year = {2010},
  month = nov,
  type = {Th\`{e}se d'habilitation},
  school = {Universit{\'e} Paris-Sud 11},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {habilitation},
  x-support = {rapport},
  topics = {team, proval}
}

@techreport{contejean08rr,
  author = {\'Evelyne Contejean and Julien Forest and Xavier Urbain},
  title = {{Deep-Embedded Unification}},
  institution = {C\'edric laboratory, CNAM Paris, France},
  year = {2008},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  type = {Research Report},
  number = {1547},
  topics = {team}
}

@inproceedings{contejean10gpl,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest
                and Andrei Paskevich and Olivier Pons and Xavier
                  Urbain},
  title = {{A3PAT, an Approach for Certified Automated Termination Proofs}},
  booktitle = {{Journ\'ees nationales du GDR-GPL}},
  year = {2010},
  editor = {\'Eric Cariou and Laurence Duchien and Yves Ledru},
  address = {{Pau, France}},
  month = mar,
  organization = {{GDR GPL}},
  topics = {team},
  x-equipes = {demons PROVAL ext},
  x-support = {actes_aux},
  x-cle-support = {JGDRGPL},
  x-type = {article},
  annote = {Invited, selected paper}
}

@techreport{contejean11rr,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest
                  and Olivier Pons and Xavier Urbain},
  title = {{Automated Certified Proofs with CiME3}},
  institution = {C\'edric laboratory, CNAM Paris, France},
  year = {2011},
  number = {2044},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  url = {http://cedric.cnam.fr/fichiers/art_2044.pdf},
  topics = {team},
  abstract = {http://www.lri.fr/~contejea/publis/rr2044/abstract.html}
}

@techreport{auger13rr1560,
  hal = {http://hal.archives-ouvertes.fr/hal-00834633},
  topics = {team},
  author = {C\'edric Auger and Zohir Bouzid and Pierre Courtieu and S\'ebastien Tixeuil and Xavier Urbain},
  title = {Certified Impossibility Results for Byzantine-Tolerant Mobile Robots},
  institution = {LRI},
  year = {2013},
  type = {Research Report},
  number = {1560},
  month = jun,
  pdf = {http://hal.archives-ouvertes.fr/docs/00/83/46/33/PDF/rr.pdf},
  url = {http://arxiv.org/abs/1306.4242}
}

@proceedings{rta98,
  title = {9th International Conference on Rewriting Techniques and
			Applications},
  booktitle = {9th International Conference on Rewriting Techniques and
			Applications},
  editor = {Tobias Nipkow},
  publisher = {Springer},
  year = 1998,
  month = apr,
  address = {Tsukuba, Japan},
  series = {Lecture Notes in Computer Science},
  volume = {1379}
}

@proceedings{rta08,
  editor = {Andrei Voronkov},
  title = {Rewriting Techniques and Applications, 19th International
               Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008,
               Proceedings},
  booktitle = {rta08},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5117},
  year = {2008},
  isbn = {978-3-540-70588-8}
}

@proceedings{rta11,
  booktitle = {22nd International Conference on Rewriting Techniques and Applications (RTA 11)},
  series = {Leibniz International Proceedings in Informatics},
  year = {2011},
  volume = {10},
  editor = {Manfred Schmidt-Schau{\ss}},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address = {Novi Sad, Serbia},
  isbn = {978-3-939897-30-9},
  issn = {1868-8969}
}

@proceedings{ijcar01,
  title = {International Joint Conference on Automated Reasoning},
  booktitle = {First International Joint Conference on Automated Reasoning},
  year = 2001,
  editor = {Rajeev Gor{\'e} and Alexander Leitsch and Tobias Nipkow},
  volume = 2083,
  series = {Lecture Notes in Artificial Intelligence},
  address = {Siena, Italy},
  month = jun,
  publisher = {Springer}
}

@proceedings{tphols2008,
  title = {Theorem Proving in Higher Order Logics:
                           21th International Conference, TPHOLs 2008},
  booktitle = {21th International Conference on Theorem Proving in Higher Order Logics},
  editor = {Otmame A{\"i}t-Mohamed and C\'esar Mu{\~n}oz and Sofi\`ene Tahar},
  series = {Lecture Notes in Computer Science},
  volume = 5170,
  year = 2008,
  addresse = {Montr\'eal, Canada},
  month = aug,
  publisher = {Springer}
}

@proceedings{wst03,
  booktitle = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}},
  title = {{Extended Abstracts of the 6th International Workshop on Termination, WST'03}},
  year = {2003},
  editor = {Albert Rubio},
  month = jun,
  note = {Technical Report DSIC II/15/03, Universidad Polit\'ecnica de Valencia, Spain}
}

@proceedings{pepm04,
  title = {Partial Evaluation and Program Manipulation},
  year = 2004,
  booktitle = {ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation},
  address = {Verona, Italy},
  month = aug,
  publisher = {ACM Press}
}

@proceedings{pepm10,
  title = {Partial Evaluation and Program Manipulation},
  year = 2010,
  booktitle = {ACM SIGPLAN 2010 Symposium on Partial Evaluation and Program Manipulation},
  editor = {John P. Gallagher and Janis Voigtl{\"a}nder},
  address = {Madrid, Spain},
  month = jan,
  publisher = {ACM Press},
  isbn = {978-1-60558-727-1}
}

@proceedings{frocos07,
  editor = {Boris Konev and Frank Wolter},
  title = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
  booktitle = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
  month = sep,
  year = 2007,
  address = {Liverpool,UK},
  publisher = {Springer},
  series = {Lecture Notes in Artificial Intelligence},
  volume = 4720,
  isbn = {978-3-540-74620-1}
}