contejean.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc contejean.cite -ob contejean.bib -c 'author : "contejean"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@misc{aggoun,
author = {Abderahmane Aggoun et Nicolas Beldiceanu and \'Evelyne Contejean},
title = {Introducing Constrained Sequences in {CHIP}},
note = {submitted}
}
@inproceedings{ajili95cp,
author = {Ajili, Farid and Contejean, \'Evelyne},
title = {Complete Solving of Linear Diophantine Equations and
Inequations without adding Variables},
crossref = {cp95},
topics = {team, cclserver, solserver, lri},
pages = {1--17},
abstract = {http://www.lri.fr/~contejea/publis/cp95/abstract.html},
type_publi = {icolcomlec},
clef_labo = {AC95E},
doi = {http://dx.doi.org/10.1007/3-540-60299-2_1}
}
@techreport{ajili95rr,
author = {Ajili, Farid and Contejean, \'Evelyne},
title = {Complete solving of linear and Diophantine equational and
inequational systems without adding variables},
institution = {INRIA},
year = 1995,
number = 0175,
month = jun
}
@article{ajili97tcs,
author = {Ajili, Farid and Contejean, \'Evelyne},
title = {Avoiding Slack Variables in the Solving of Linear
Diophantine Equations and Inequations},
journal = {Theoretical Computer Science},
year = 1997,
volume = 173,
number = 1,
month = feb,
pages = {183--208},
editor = {U. Montanari and F. Rossi},
abstract = {http://www.lri.fr/~contejea/publis/1997tcs/abstract.html},
type_publi = {irevcomlec},
topics = {team, cclserver, solserver, lri},
annote = {Special Issue of TCS dedicated to a refereed
selection of papers presented at CP'95},
type_publi = {AC97R},
doi = {http://dx.doi.org/10.1016/S0304-3975(96)00195-8}
}
@inproceedings{beldiceanu93,
author = {Nicolas Beldiceanu and \'Evelyne Contejean and
Helmut Simonis},
topics = {team, constraints, linear Diophantine equations},
location = {EC},
title = {Integrating an algorithm for solving linear constraints
in finite domains in the language {CHIP}},
booktitle = {Proc. 4th Workshop on Constraint Logic Programming},
month = mar,
year = 1993,
abstract = {http://www.lri.fr/~contejea/publis/1993wclp/abstract.html}
}
@article{beldiceanu94jmcm,
author = {Nicolas Beldiceanu and \'Evelyne Contejean},
topics = {team, lri},
title = {Introducing global constraints in {CHIP}},
journal = {Journal of {M}athematical and Computer Modelling},
year = 1994,
volume = 20,
number = 12,
pages = {97--123},
location = {biblio-equipe},
abstract = {http://www.lri.fr/~contejea/publis/jmcm94/abstract.html},
http = {http://dx.doi.org/10.1016/0895-7177(94)90127-9},
type_publi = {irevcomlec},
clef_labo = {BC94R}
}
@inproceedings{beldiceanu98informs,
author = {Nicolas Beldiceanu and \'Eric Bourreau and \'Evelyne Contejean},
title = {Solving a Hard Vehicle Routing \& Loading Problem},
booktitle = {Proceedings of the Spring Meeting of the Institute for
Operations Research and the Management Sciences},
year = 1998,
address = {Montreal},
month = apr,
type_publi = {colloque},
topics = {team, lri},
clef_labo = {BBC98N},
abstract = {http://www.lri.fr/~contejea/publis/informs98/abstract.html}
}
@inproceedings{boudet90lics,
topics = {unification, old-team},
author = {Alexandre Boudet and \'Evelyne Contejean and
Herv{\'e} Devie},
title = {A new {AC}-unification algorithm with a new
algorithm for solving diophantine equations},
crossref = {lics90},
pages = {289--299},
abstract = {http://www.lri.fr/~contejea/publis/1990lics/abstract.html},
doi = {http://dx.doi.org/10.1109/LICS.1990.113755}
}
@inproceedings{boudet92alp,
author = {Alexandre Boudet and \'Evelyne Contejean},
topics = {old-team},
title = {On $n$-syntactic equational theories},
pages = {446--457},
crossref = {alp92},
year = 1992,
abstract = {http://www.lri.fr/~contejea/publis/1992alp/abstract.html},
doi = {http://dx.doi.org/10.1007/BFb0013843}
}
@inproceedings{boudet94ccl,
author = {Alexandre Boudet and \'Evelyne Contejean},
topics = {team, cclserver, lri},
title = {``{S}yntactic'' {AC}-Unification},
pages = {136--151},
crossref = {ccl94},
year = 1994,
abstract = {http://www.lri.fr/~contejea/publis/ccl94/abstract.html},
http = {http://dx.doi.org/10.1007/BFb0016849},
type_publi = {icolcomlec},
clef_labo = {BC94E}
}
@inproceedings{boudet96rta,
author = {Alexandre Boudet and \'Evelyne Contejean and Claude
March{\'e}},
title = {{AC}-complete unification and its application to
theorem proving},
topics = {team, cclserver, lri},
year = 1996,
crossref = {rta96},
pages = {18--32},
x-pdf = {http://www.lri.fr/~marche/articles/rta96.ps.gz},
abstract = {http://www.lri.fr/~marche/rta96.html},
doi = {http://dx.doi.org/10.1007/3-540-61464-8_40},
type_publi = {icolcomlec},
clef_labo = {BCM96E}
}
@inproceedings{boudet97cp,
author = {Alexandre Boudet and \'Evelyne Contejean},
title = {{AC}-Unification of Higher-order Patterns},
crossref = {cp97},
year = 1997,
abstract = {http://www.lri.fr/~contejea/publis/1997cp/abstract.html},
doi = {http://dx.doi.org/10.1007/BFb0017445},
type_publi = {icolcomlec},
topics = {team, cclserver, lri},
pages = {267--281},
clef_labo = {BC97E}
}
@inproceedings{boudet98cade,
author = {Alexandre Boudet and \'Evelyne Contejean},
title = {{About the Confluence of Equational Pattern Rewrite
Systems}},
crossref = {cade98},
type_publi = {icolcomlec},
topics = {team, cclserver, lri},
pages = {88--102},
doi = {http://dx.doi.org/10.1007/BFb0054250},
abstract = {http://www.lri.fr/~contejea/publis/1998cade/abstract.html},
clef_labo = {BC98E}
}
@misc{contejean88,
author = {\'Evelyne Contejean},
topics = {diophantine equations, old-teamnop},
location = {Evelyne},
title = {Unification associative-commutative},
howpublished = {M{\'e}moire de DEA , Universit{\'e} de Paris Sud, Orsay},
year = 1988
}
@inproceedings{contejean89,
author = {\'Evelyne Contejean and Herv{\'e} Devie},
topics = {unification, old-team},
title = {Solving systems of linear Diophantine equations},
booktitle = {Proc. 3rd Workshop on Unification, Lambrecht, Germany},
year = 1989,
month = jun,
publisher = {University of Kaiserslautern}
}
@article{contejean91,
author = {\'Evelyne Contejean and Herv{\'e} Devie},
topics = {old-team},
location = {HC 388},
title = {R{\'e}solution de syst{\`e}mes lin{\'e}aires
d'{\'e}quations diophantiennes},
journal = {Comptes-Rendus de l'Acad{\'e}mie des Sciences de Paris},
year = 1991,
volume = 313,
note = {S{\'e}rie I},
pages = {115-120},
abstract = {
Nous pr\'esentons ici un algorithme pour r\'esoudre les syst\`emes lin\'eaires
homog\`enes d'\'equations diophantiennes de fa\c{c}on directe, \`a l'aide d'une
interpr\'etation g\'eom\'etrique.
}
}
@phdthesis{contejean92these,
author = {\'Evelyne Contejean},
title = {{\'E}l{\'e}ments pour la D{\'e}cidabilit{\'e} de
l'Unification modulo la Distributivit{\'e}},
school = {Universit{\'e} Paris-Sud},
year = 1992,
address = {Orsay, France},
month = apr,
type = {Th{\`e}se de Doctorat},
topics = {unification, old-team},
type_publi = {these}
}
@inproceedings{contejean93icalp,
author = {\'Evelyne Contejean},
topics = {unification, team, lri},
title = {A Partial Solution for {D}-unification based on a Reduction
to {AC1}-unification},
pages = {621--632},
crossref = {icalp93},
year = 1993,
abstract = {http://www.lri.fr/~contejea/publis/1993icalp/abstract.html},
type_publi = {icolcomlec},
doi = {http://dx.doi.org/10.1007/3-540-56939-1_107}
}
@inproceedings{contejean93iclp,
author = {\'Evelyne Contejean},
topics = {Diophantine constraints, team, lri},
title = {Solving Linear Diophantine Constraints Incrementally},
crossref = {iclp93},
pages = {532--549},
abstract = {http://www.lri.fr/~contejea/publis/1993iclp/abstract.html},
type_publi = {icolcomlec}
}
@article{contejean93jsc,
author = {\'Evelyne Contejean},
topics = {unification, distributivity, team, lri},
title = {Solving {$*$}-problems modulo Distributivity by a
Reduction to {$AC1$}-unification},
journal = {Journal of Symbolic Computation},
year = 1993,
volume = 16,
number = 5,
pages = {493-52},
abstract = {http://www.lri.fr/~contejea/publis/1993jsc/abstract.html},
type_publi = {irevcomlec},
doi = {http://dx.doi.org/10.1006/jsco.1993.1060}
}
@article{contejean94ic,
author = {\'Evelyne Contejean and Herv{\'e} Devie},
topics = {Diophantine constraints, team, lri, solserver},
title = {An Efficient Algorithm for Solving Systems of Diophantine
Equations},
journal = {Information and Computation},
year = 1994,
volume = 113,
number = 1,
month = aug,
pages = {143--172},
ftp = {ftp://ftp.lri.fr/LRI/articles/contejean/ic94.ps.gz},
abstract = {http://www.lri.fr/~contejea/publis/1994ic.html},
type_publi = {irevcomlec},
clef_labo = {CD94Rb}
}
@inproceedings{contejean96rta,
author = {\'Evelyne Contejean and Claude March{\'e}},
title = {{CiME: Completion Modulo $E$}},
crossref = {rta96},
pages = {416--419},
year = 1996,
note = {System Description available at \url{http://cime.lri.fr/}},
x-pdf = {http://www.lri.fr/~marche/articles/cime-rta96.ps.gz},
abstract = {http://www.lri.fr/~marche/cime-rta96.html},
url = {http://cime.lri.fr/},
doi = {http://dx.doi.org/10.1007/3-540-61464-8_70},
type_publi = {icolcomlec},
topics = {team, lri, cclserver},
clef_labo = {CM96E}
}
@techreport{contejean97rr,
author = {\'Evelyne Contejean and Claude March{\'e} and Landy Rabehasaina},
title = {Rewrite systems for natural, integral, and rational
arithmetic},
institution = {Laboratoire de Recherche en Informatique},
year = 1997,
type = {Research Report},
address = {Universit{\'e} de Paris-Sud, Orsay, France}
}
@inproceedings{contejean97rta,
author = {\'Evelyne Contejean and Claude March{\'e} and Landy Rabehasaina},
title = {Rewrite systems for natural, integral, and rational
arithmetic},
pages = {98-112},
crossref = {rta97},
year = 1997,
x-pdf = {http://www.lri.fr/~marche/articles/rta97.ps.gz},
doi = {http://dx.doi.org/10.1007/3-540-62950-5_64},
abstract = {http://www.lri.fr/~marche/rta97.html},
type_publi = {icolcomlec},
topics = {team, lri, cclserver},
clef_labo = {CMR97E}
}
@misc{SOLsurvol95,
author = {Ajili, F. and Contejean, E. and Domenjoud, E.
and Filgueiras, M. and Kirchner, C. and Tom{\'a}s, A.-P.},
title = {{Solving Linear Diophantine Equations: The State of the Art}},
howpublished = {in preparation},
year = 1995
}
@unpublished{contejean89unif,
author = {{\'E}velyne Contejean and Herv{\e'} Devie},
title = {{Solving Systems of Linear Diophantine Equations}},
note = {UNIF'89},
year = 1989,
month = jun,
address = {Lambrecht, Germany}
}
@unpublished{contejean91unif,
author = {Alexandre Boudet and {\'E}velyne Contejean},
title = {{$n$-syntactic Theories}},
note = {UNIF'91},
year = 1991,
address = {Barbizon, France},
month = jul
}
@unpublished{contejean92unif,
author = {{\'E}velyne Contejean},
title = {{Unification Problems Modulo Distributivity}},
note = {UNIF'92},
year = 1992,
address = {Dagstuhl, Germany},
moth = jul
}
@unpublished{contejean95unif,
author = {Farid Ajili and {\'E}velyne Contejean},
title = {{Complete Solving of Diophantine Equational and Inequational
Systems without Adding Slack Variables }},
note = {UNIF'95},
year = 1995,
address = {Sitges, Spain},
month = apr
}
@unpublished{contejean96unif,
author = {Alexandre Boudet and {\'E}velyne Contejean and Claude March{\'e}},
title = {{AC Complete Unification and its Application to Theorem Proving}},
note = {UNIF'96},
year = 1996,
address = {Herrsching, Germany},
month = jun
}
@unpublished{contejean97unif,
author = {Alexandre Boudet and {\'E}velyne Contejean},
title = {{AC-Unification of Higher-order Patterns}},
note = {UNIF'97},
year = 1997,
address = {Orl{\'e}ans, France},
month = may
}
@unpublished{contejean98unif,
author = {Alexandre Boudet and {\'E}velyne Contejean},
title = {{About the Confluence of Equational Pattern Rewriting Systems}},
note = {UNIF'98},
year = 1998,
address = {Rome, Italy},
month = jun
}
@inproceedings{boudet01rta,
author = {Alexandre Boudet and Evelyne Contejean},
title = {{Combining Pattern $E$-unification Algorithms}},
crossref = {rta01},
pages = {63--76},
type_publi = {icolcomlec},
topics = {rewriting, team, lri, cclserver},
doi = {http://dx.doi.org/10.1007/3-540-45127-7_7},
abstract = {http://www.lri.fr/~contejea/publis/2001rta/abstract.html}
}
@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}
}
@unpublished{benzaken18,
author = {{V\'eronique Benzaken and \'Evelyne Contejean and Chantal Keller and Eunice Martins}},
title = {{COQ specification and verification of SQL's query execution plans}}
}
@inproceedings{benzaken17itp,
author = {V{\'{e}}ronique Benzaken and
Evelyne Contejean and
Stefania Dumbrava},
title = {Certifying Standard and Stratified Datalog Inference Engines in SSReflect},
booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP}
2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
pages = {171--188},
year = {2017},
crossref = {itp2017},
url = {https://doi.org/10.1007/978-3-319-66107-0_12},
doi = {10.1007/978-3-319-66107-0_12}
}
@unpublished{benzaken16hal,
title = {{SQLCert: Coq mechanisation of SQL's compilation: Formally reconciling SQL and (relational) algebra}},
author = {Benzaken, V{\'e}ronique and Contejean, Evelyne},
url = {https://hal.archives-ouvertes.fr/hal-01487062},
note = {working paper or preprint},
year = {2016},
month = oct,
pdf = {https://hal.archives-ouvertes.fr/hal-01487062/file/main.pdf},
hal_id = {hal-01487062},
hal_version = {v1}
}
@inproceedings{benzaken14esop,
hal = {http://hal.inria.fr/hal-00924156},
author = {V\'eronique Benzaken and \'Evelyne Contejean and Stefania Dumbrava},
title = {A {Coq} Formalization of the Relational Data Model},
crossref = {esop2014},
year = 2014,
month = apr,
editor = {Z. Shao},
booktitle = {European Symposium on Programming, LNCS 8410},
pages = {189-208},
type_publi = {icolcomlec},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes}
}
@techreport{conchon10rr,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
institution = {{LRI, Universit\'e Paris Sud}},
year = 2010,
type = {Research Report},
number = 1538,
month = dec,
topics = {team, lri},
type_publi = {interne},
type_digiteo = {no},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {rapport},
x-pdf = {http://www.lri.fr/~bibli/Rapports-internes/2010/RR1538.pdf},
url = {http://www.lri.fr/~bibli/Rapports-internes/2010/RR1538.pdf},
abstract = {http://www.lri.fr/~contejea/publis/rr1538/abstract.html}
}
@inproceedings{conchon11tacas,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
crossref = {tacas2011},
year = 2011,
month = apr,
type_publi = {icolcomlec},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {TACAS},
url = {http://proval.lri.fr/publications/conchon11tacas.pdf},
hal = {http://hal.inria.fr/hal-00777663},
pages = {45-59},
doi = {10.1007/978-3-642-19835-9_6},
abstract = {http://www.lri.fr/~contejea/publis/2011tacas/abstract.html}
}
@article{conchon12lmcs,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {Canonized Rewriting and Ground {AC} Completion Modulo {Shostak} Theories : Design and Implementation},
journal = {Logical Methods in Computer Science},
year = {2012},
month = sep,
pages = {1--29},
volume = 8,
number = 3,
hal = {http://hal.inria.fr/hal-00798082},
url = {http://www.lmcs-online.org/ojs/viewarticle.php?id=1037&layout=abstract&iid=40},
topics = {team},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-international-audience = {yes},
x-editorial-board = {yes},
x-cle-support = {LMCS},
doi = {10.2168/LMCS-8(3:16)2012},
note = {Selected Papers of the Conference \emph{Tools and Algorithms for the Construction and Analysis of Systems} (TACAS 2011), Saarbr{\"u}cken, Germany, 2011}
}
@inproceedings{conchon10lpar,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Ground Associative and Commutative Completion Modulo Shostak Theories}},
booktitle = {LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
year = 2010,
editor = {Andrei Voronkov},
series = {EasyChair Proceedings},
address = {Yogyakarta, Indonesia},
month = oct,
note = {(short paper)},
type_publi = {colloque},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {LPAR}
}
@inproceedings{conchon07afm,
author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig and St{\'e}phane Lescuyer},
title = {{Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant}},
crossref = {afm07},
abstract = {Ergo is a little engine of proof dedicated to program
verification. It fully supports quantifiers and directly handles
polymorphic sorts. Its core component is CC(X), a new combination
scheme for the theory of uninterpreted symbols parameterized by a
built-in theory X. In order to make a sound integration in a proof
assistant possible, Ergo is capable of generating proof traces
for CC(X). Alternatively, Ergo can also be called interactively
as a simple oracle without further verification. It is currently
used to prove correctness of C and Java programs as part of the Why
platform.},
abstract = {http://www.lri.fr/~contejea/publis/2007afm/abstract.html},
topics = {team,lri},
type_digiteo = {conf_isbn},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {AFM},
x-pdf = {http://fm.csl.sri.com/AFM07/afm07-preprint.pdf},
url = {http://fm.csl.sri.com/AFM07/afm07-preprint.pdf},
doi = {10.1145/1345169.1345176},
pages = {55--59}
}
@inproceedings{conchon07smt,
author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig},
title = {{CC(X)}: Efficiently Combining Equality and Solvable Theories without Canonizers},
booktitle = {SMT 2007: 5th International Workshop on Satisfiability Modulo},
year = 2007,
editor = {Sava Krstic and Albert Oliveras},
topics = {team,lri},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {SMT}
}
@inproceedings{conchon08smt,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean
and St\'ephane Lescuyer},
title = {{Implementing Polymorphism in SMT solvers}},
booktitle = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
pages = {1--5},
year = 2008,
editor = {Clark Barrett and Leonardo de Moura},
volume = 367,
series = {ACM International Conference Proceedings Series},
topics = {team,lri},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {SMT},
x-pdf = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
url = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
isbn = {978-1-60558-440-9},
doi = {10.1145/1512464.1512466},
abstract = {http://www.lri.fr/~contejea/publis/2008smt/abstract.html}
}
@misc{conchonijcar06,
author = {Sylvain Conchon and \'Evelyne Contejean},
title = {Rule Based Incremental Congruence Closure with Commutative
Symbols},
month = mar,
year = 2006
}
@inproceedings{conchon08entcs,
author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig and St\'ephane Lescuyer},
title = {{CC(X)}: Semantical Combination of Congruence Closure with
Solvable Theories},
booktitle = {Post-proceedings of the 5th International Workshop on
Satisfiability Modulo Theories ({SMT 2007})},
series = {Electronic Notes in Computer Science},
publisher = {Elsevier Science Publishers},
volume = {198(2)},
pages = {51--69},
year = 2008,
abstract = {
We present a generic congruence closure algorithm for deciding
ground formulas in the combination of the theory of equality with
uninterpreted symbols and an arbitrary built-in solvable theory X.
Our algorithm CC(X) is reminiscent of Shostak combination: it
maintains a union-find data-structure modulo X from which maximal
information about implied equalities can be directly used for
congruence closure. CC(X) diverges from Shostak's approach by the use
of semantical values for class representatives instead of canonized
terms. Using semantical values truly reflects the actual
implementation of the decision procedure for X. It also enforces to
entirely rebuild the algorithm since global canonization, which is
at the heart of Shostak combination, is no longer feasible with
semantical values. CC(X) has been implemented in Ocaml and is at
the core of Ergo, a new automated theorem prover dedicated to
program verification.
},
abstract = {http://www.lri.fr/~contejea/publis/2008entcs/abstract.html},
topics = {team},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-cle-support = {ENTCS},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
doi = {10.1016/j.entcs.2008.04.080}
}
@inproceedings{contejean00rta,
author = {\'Evelyne Contejean and Antoine Coste and Benjamin Monate},
title = {Rewriting Techniques in Theoretical Physics},
crossref = {rta00},
pages = {80--94},
year = 2000,
topics = {team,lri},
type_publi = {icolcomlec},
doi = {10.1007/10721975_6},
abstract = {http://www.lri.fr/~contejea/publis/2000rta/abstract.html}
}
@inproceedings{contejean01symcon,
author = {\'Evelyne Contejean and Ana Paula Tomas},
title = {{On Symmetries in Systems Coming from AC-Unification of
Higher-Order Patterns}},
booktitle = {{SymCon'01, Symmetry in Constraints}},
year = 2001,
editor = {Pierre Flener and Justin Pearson},
address = {Paphos, Cyprus},
month = {December},
topics = {team,lri},
type_publi = {colloque}
}
@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}
}
@inproceedings{contejean04rta,
author = {\'Evelyne Contejean},
title = {{A certified AC matching algorithm}},
booktitle = {15th International Conference on Rewriting Techniques and Applications},
crossref = {rta04},
pages = {70--84},
year = 2004,
type_publi = {icolcomlec},
topics = {team},
doi = {10.1007/978-3-540-25979-4_5},
abstract = {http://www.lri.fr/~contejea/publis/2004rta/abstract.html}
}
@inproceedings{contejean05cade,
author = {\'Evelyne Contejean and Pierre Corbineau},
title = {Reflecting Proofs in First-Order Logic with Equality},
type_publi = {icolcomlec},
topics = {team},
pages = {7--22},
crossref = {cade05},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {CADE},
abstract = {http://www.lri.fr/~contejea/publis/2005cade/abstract.html},
doi = {10.1007/11532231_2}
}
@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}
}
@incollection{contejean07jpj,
author = {\'Evelyne Contejean},
title = {Modelling permutations in {Coq} for {Coccinelle}},
crossref = {jpj07},
pages = {259--269},
doi = {10.1007/978-3-540-73147-4_13},
abstract = {http://www.lri.fr/~contejea/publis/2007jpj/abstract.html},
type_publi = {chapitre},
type_digiteo = {chapitre},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {chapitre},
x-support = {ouvrage}
}
@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}
}
@inproceedings{contejean08types,
author = {\'Evelyne Contejean},
title = {{Coccinelle, a Coq library for rewriting}},
booktitle = {Types},
year = 2008,
address = {Torino, Italy},
month = mar,
type_publi = {autre},
x-equipes = {demons PROVAL},
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}
}
@misc{coccinelle,
author = {\'Evelyne Contejean},
title = {{Coccinelle}},
year = 2005,
url = {{http://www.lri.fr/~contejea/Coccinelle/coccinelle.html}},
note = {\url{http://www.lri.fr/~contejea/Coccinelle/coccinelle.html}},
topics = {team,lri},
type_publi = {autre},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@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
}
@misc{alt-ergo,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala and St\'ephane Lescuyer and Alain Mebsout},
title = {The {Alt-Ergo} Automated Theorem Prover},
note = {\url{http://alt-ergo.lri.fr/}},
topics = {team,lri},
year = 2008,
x-equipes = {demons PROVAL}
}
@misc{ergo,
author = {Sylvain Conchon and \'Evelyne Contejean},
title = {The {Alt-Ergo} automatic Theorem Prover},
url = {http://alt-ergo.lri.fr/},
howpublished = {\url{http://alt-ergo.lri.fr/}},
note = {APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000},
topics = {team,lri},
year = 2008,
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@misc{altergo10app,
author = {Sylvain Conchon and \'Evelyne Contejean},
title = {Alt-Ergo},
howpublished = {APP Deposit},
month = mar,
year = 2010,
note = {IDDN.FR.001.110026.000.S.P.2010.000.10000},
annote = {\url{http://alt-ergo.lri.fr}}
}
@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}
}
@inproceedings{bobot12ijcar,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and
\'Evelyne Contejean and Mohamed Iguernelala and
Assia Mahboubi and Alain Mebsout and Guillaume Melquiond},
title = {A {Simplex}-Based Extension of {Fourier-Motzkin} for
Solving Linear Integer Arithmetic},
booktitle = {IJCAR 2012: Proceedings of the 6th International Joint
Conference on Automated Reasoning},
year = {2012},
editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
series = {Lecture Notes in Computer Science},
address = {Manchester, UK},
month = jun,
volume = {7364},
pages = {67--81},
hal = {http://hal.inria.fr/hal-00687640},
doi = {10.1007/978-3-642-31365-3_8},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
x-cle-support = {IJCAR},
type_publi = {icolcomlec},
publisher = {Springer},
abstract = {This paper describes a novel decision procedure for
quantifier-free linear integer arithmetic. Standard
techniques usually relax the initial problem to the
rational domain and then proceed either by
projection (e.g. Omega-Test) or by branching/cutting
methods (branch-and-bound, branch-and-cut, Gomory
cuts). Our approach tries to bridge the gap between
the two techniques: it interleaves an exhaustive
search for a model with bounds inference. These
bounds are computed provided an oracle capable of
finding constant positive linear combinations of
affine forms. We also show how to design an
efficient oracle based on the Simplex procedure. Our
algorithm is proved sound, complete, and terminating
and is implemented in the Alt-Ergo theorem
prover. Experimental results are promising and show
that our approach is competitive with
state-of-the-art SMT solvers.}
}
@phdthesis{contejean14hdr,
hal = {https://hal.inria.fr/tel-01089490},
author = {{\'E}velyne Contejean},
title = {{Facettes de la preuve, Jeux de reflets entre d{\'e}monstration automatique et preuve assist{\'e}}},
year = 2014,
month = jun,
type = {Th{\`e}se d'habilitation},
school = {Universit{\'e} Paris-Sud},
type_publi = {these},
note = {\url{https://www.lri.fr/~contejea/dossiers/hdr/hdr.pdf}},
rawebnote = {\url{https://www.lri.fr/~contejea/dossiers/hdr/hdr.pdf}},
x-equipes = {demons PROVAL},
x-type = {habilitation},
x-support = {rapport},
topics = {team}
}
@proceedings{afm07,
title = {{Proceedings of the second workshop on Automated formal methods}},
booktitle = {{Proceedings of the second workshop on Automated formal methods}},
year = 2007,
editor = {John Rushby and N. Shankar},
publisher = {ACM Press},
isbn = {978-1-59593-879-4}
}
@proceedings{alp92,
title = {3th International Conference on Algebraic and
Logic Programming},
booktitle = {3th International Conference on Algebraic and
Logic Programming},
editor = {H{\'e}l{\`e}ne Kirchner and Giorgio Levi},
month = sep,
year = 1992,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {632},
address = {Volterra, Italy},
isbn = {3-540-55873-X}
}
@proceedings{cade98,
title = {15th International Conference on Automated Deduction},
booktitle = {15th International Conference on Automated Deduction},
address = {Lindau, Germany},
editor = {C. and H. Kirchner},
year = 1998,
month = jul,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
isbn = {3-540-64675-2},
volume = 1421
}
@proceedings{cade05,
title = {20th International Conference on Automated Deduction},
booktitle = {20th International Conference on Automated Deduction (CADE-20)},
address = {Tallinn, Estonia},
month = jul,
year = 2005,
editor = {Robert Nieuwenhuis},
series = {Lecture Notes in Artificial Intelligence},
volume = 3632,
publisher = {Springer},
isbn = {3-540-28005-7}
}
@proceedings{ccl94,
topics = {teamp, cclserver,lri},
title = {First International Conference on Constraints in
Computational Logics},
booktitle = {First International Conference on Constraints in
Computational Logics},
editor = {Jean-Pierre Jouannaud},
address = {M{\"u}nchen, Germany},
month = sep,
year = 1994,
series = {Lecture Notes in Computer Science},
volume = 845,
publisher = {Springer},
isbn = {3-540-58403-X},
type_publi = {editeur}
}
@proceedings{cp95,
title = {Principles and Practice of Constraint Programming},
booktitle = {Proc. First International Conference on Principles and Practice of Constraint Programming},
year = 1995,
editor = {Ugo Montanari and Francesca Rossi},
publisher = {Springer},
address = {Cassis, France},
month = sep,
series = {Lecture Notes in Computer Science},
volume = 976,
isbn = {3-540-60299-2}
}
@proceedings{cp97,
title = {Principles and Practice of Constraint Programming},
booktitle = {Principles and Practice of Constraint Programming},
year = 1997,
editor = {Gert Smolka},
publisher = {Springer},
address = {Linz, Austria},
month = oct,
series = {Lecture Notes in Computer Science},
volume = 1330,
isbn = {3-540-63753-2}
}
@proceedings{icalp93,
title = {20th International Colloquium on
Automata, Languages and Programming},
booktitle = {20th International Colloquium on
Automata, Languages and Programming},
address = {Lund, Sweden},
editor = {Andrzej Lingas and Rolf Karlsson and Svante Carlsson},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {700},
year = 1993,
month = jul,
isbn = {3-540-56939-1}
}
@proceedings{iclp93,
title = {Proceedings of the 10th International Conference on
Logic Programming},
booktitle = {Proceedings of the 10th International Conference on
Logic Programming},
series = {Logic Programming},
year = 1993,
month = jun,
address = {Budapest, Hungary},
editor = {David S. Warren},
publisher = {MIT Press},
isbn = {0-262-73105-3}
}
@proceedings{lics90,
title = {Proceedings of the Fifth Annual IEEE Symposium on Logic
in Computer Science},
booktitle = {Proceedings of the Fifth Annual IEEE Symposium on Logic
in Computer Science},
year = 1990,
month = jun,
address = {Philadelphia, Pennsylvania, USA},
publisher = {{IEEE} Comp. Soc. Press},
isbn = {0-8186-2073-0}
}
@proceedings{rta96,
title = {7th International Conference on Rewriting Techniques and
Applications},
booktitle = {7th International Conference on Rewriting Techniques and
Applications},
editor = {Harald Ganzinger},
publisher = {Springer},
year = 1996,
month = jul,
address = {New Brunswick, NJ, USA},
series = {Lecture Notes in Computer Science},
volume = 1103,
isbn = {3-540-61464-8}
}
@proceedings{rta97,
title = {8th International Conference on Rewriting Techniques and
Applications},
booktitle = {8th International Conference on Rewriting Techniques and
Applications},
editor = {Hubert Comon},
publisher = {Springer},
year = 1997,
month = jun,
address = {Barcelona, Spain},
series = {Lecture Notes in Computer Science},
volume = {1232},
isbn = {3-540-62950-5}
}
@proceedings{rta00,
title = {11th International Conference on Rewriting Techniques and Applications},
booktitle = {11th International Conference on Rewriting Techniques and Applications},
editor = {Leo Bachmair},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 1833,
month = jul,
year = 2000,
address = {Norwich, UK},
isbn = {3-540-67778-X}
}
@proceedings{rta01,
title = {12th International Conference on Rewriting Techniques and Applications},
booktitle = {12th International Conference on Rewriting Techniques and Applications},
editor = {Aart Middeldorp},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 2051,
month = may,
year = 2001,
address = {Utrecht, The Netherlands},
isbn = {3-540-42117-3}
}
@proceedings{rta04,
title = {15th International Conference on Rewriting Techniques and Applications},
booktitle = {15th International Conference on Rewriting Techniques and Applications},
editor = {Vincent van Oostrom},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 3091,
month = jun,
year = 2004,
address = {Aachen, Germany},
isbn = {3-540-22153-0}
}
@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{tacas2011,
title = {Tools and Algorithms for the Construction and Analysis of Systems},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
year = 2011,
month = apr,
editor = {Parosh A. Abdulla and K. Rustan M. Leino},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6605},
isbn = {978-3-642-19834-2},
address = {Saarbr{\"u}cken, Germany}
}
@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{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{jpj07,
title = {Rewriting, Computation and Proof},
booktitle = {Rewriting, Computation and Proof},
year = 2007,
editor = {Hubert Comon-Lundth and Claude Kirchner and H{\'e}l{\`e}ne Kirchner},
volume = 4600,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
note = {Jouannaud Festschrift},
isbn = {978-3-540-73146-7}
}
@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}
}
@proceedings{esop2014,
title = {23rd European Symposium on Programming (ESOP)},
year = 2014,
booktitle = {ESOP},
editor = {Zhong Shao},
series = {Lecture Notes in Computer Science},
address = {Grenoble},
month = apr,
publisher = {Springer}
}
@proceedings{itp2017,
editor = {Mauricio Ayala{-}Rinc{\'{o}}n and
C{\'{e}}sar A. Mu{\~{n}}oz},
title = {Interactive Theorem Proving - 8th International Conference, {ITP}
2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10499},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-66107-0},
doi = {10.1007/978-3-319-66107-0},
isbn = {978-3-319-66106-3}
}