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}
}