lescuyer.bib

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

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

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

@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{Conchon08jfla,
  author = {Sylvain Conchon and Johannes Kanig and St\'ephane Lescuyer},
  title = {{SAT-MICRO : petit mais costaud !}},
  year = 2008,
  topics = {team, lri},
  type_publi = {colcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  x-editorial-board = {yes},
  x-international-audience = {no},
  x-proceedings = {yes},
  crossref = {jfla08},
  address = {\'Etretat, France},
  publisher = {INRIA},
  url = {http://www.lri.fr/~conchon/publis/conchon-jfla08.ps},
  abstract = {
  Le probl\`eme SAT, qui consiste `a d\'eterminer si une formule bool\'eenne
  est satisfaisable, est un des probl\`emes NP-complets les plus
  c\'el\`ebres et aussi un des plus \'etudi\'es. Bas\'es initialement sur la
  proc\'edure DPLL, les SAT-solvers modernes ont connu des
  progr\`es spectaculaires ces dix derni\`eres ann\'ees dans leurs
  performances, essentiellement gr\^ace \`a deux optimisations: le retour
  en arri\`ere non-chronologique et l'apprentissage par analyse des
  clauses conflits. Nous proposons dans cet article une \'etude formelle
  du fonctionnement de ces techniques ainsi qu'une r\'ealisation en Ocaml
  d'un SAT-solver, baptis\'e SAT-MICRO, int\'egrant ces
  optimisations. Le fonctionnement de SAT-MICRO est d\'ecrit par un
  ensemble de r\`egles d'inf\'erence et la taille de son code, 70 lignes
  au total, permet d'envisager sa certification compl\`ete.}
}

@inproceedings{couchot07cade,
  author = {Jean-Fran\c{c}ois Couchot and St\'ephane Lescuyer},
  title = {Handling Polymorphism in Automated Deduction},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CADE},
  pages = {263--278},
  booktitle = {21th International Conference on Automated Deduction (CADE-21)},
  address = {Bremen, Germany},
  month = jul,
  year = 2007,
  series = {LNCS (LNAI)},
  volume = 4603,
  x-pdf = {http://www.lri.fr/~couchot/IMG/pdf_CADE_couchot_lescuyer.pdf},
  url = {http://www.lri.fr/~couchot/IMG/pdf_CADE_couchot_lescuyer.pdf},
  abstract = {Polymorphism has become a common way of designing short and reusable
programs by abstracting generic definitions from type-specific ones.
Such a convenience is valuable in logic as well, because it unburdens
the specifier from writing redundant declarations of logical
symbols.
However,
top shelf automated theorem provers  such as
Simplify, Yices or other SMT-LIB ones do not handle polymorphism. To
this end, we present
efficient reductions of polymorphism in both unsorted and many-sorted
first order logics.
For each encoding, we show that the formulas and their encoded
counterparts are logically equivalent in the context of automated
theorem proving. The efficiency keynote is to disturb the prover as
little as possible, especially the internal decision procedures used for
special sorts, e.g. integer linear arithmetic, to which we apply a
special treatment.
The corresponding implementations are presented in the framework of
the Why/Caduceus
toolkit.}
}

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

@mastersthesis{lescuyer06master,
  author = {St\'ephane Lescuyer},
  title = {Codage de la logique du premier ordre polymorphe multi-sort\'ee
dans la logique sans sortes},
  school = {Master Parisien de Recherche en Informatique},
  topics = {team},
  type_publi = {rapport},
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport},
  year = 2006
}

@inproceedings{lescuyer08tpholset,
  author = {St\'ephane Lescuyer and Sylvain Conchon},
  title = {A Reflexive Formalization of a {SAT} Solver in {Coq}},
  booktitle = {Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics},
  year = 2008,
  topics = {team},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {?},
  x-international-audience = {yes},
  x-proceedings = {yes}
}

@inproceedings{mlpost09jfla,
  author = {Romain Bardou and Jean-Christophe Filli\^atre and Johannes Kanig and St\'ephane Lescuyer},
  title = {{Faire bonne figure avec Mlpost}},
  url = {https://usr.lmf.cnrs.fr/~jcf/publis/mlpost-fra.pdf},
  abstract = {Cet article pr\'esente Mlpost, une biblioth\`eque Ocaml de dessin
  scientifique. Elle s'appuie sur Metapost, qui permet notamment
  d'inclure des fragments \LaTeX\ dans les figures. Ocaml offre une
  alternative s\'eduisante aux langages de macros \LaTeX, aux langages
  sp\'ecialis\'es ou m\^eme aux outils graphiques. En particulier,
  l'utilisateur de Mlpost b\'en\'eficie de toute l'expressivit\'e
  d'Ocaml et de son typage statique. Enfin Mlpost propose un style
  d\'eclaratif qui diff\`ere de celui, souvent imp\'eratif, des outils existants.},
  topics = {team, lri},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla09}
}

@inproceedings{LescuyerConchon09frocos,
  author = {St{\'e}phane Lescuyer and Sylvain Conchon},
  title = {Improving {Coq} Propositional Reasoning using a Lazy {CNF} Conversion Scheme},
  topics = {team},
  x-support = {actes},
  pages = {287-303},
  doi = {10.1007/978-3-642-04222-5_18},
  crossref = {frocos09}
}

@phdthesis{lescuyer11these,
  author = {St{\'e}phane Lescuyer},
  title = {Formalisation et d\'eveloppement d'une tactique r\'eflexive pour la
d\'emonstration automatique en {Coq}},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {these},
  url = {http://proval.lri.fr/publications/lescuyer11these.pdf},
  hal = {http://tel.archives-ouvertes.fr/tel-00713668},
  topics = {team},
  year = 2011,
  month = jan
}

@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{jfla08,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2008,
  booktitle = {Dix-neuvi\`emes  Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  publisher = {INRIA}
}

@proceedings{jfla09,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2009,
  booktitle = {Vingti\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Saint-Quentin sur Is\`ere},
  publisher = {INRIA},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes}
}

@proceedings{frocos09,
  editor = {Silvio Ghilardi and
               Roberto Sebastiani},
  title = {Frontiers of Combining Systems, 7th International Symposium,
               FroCoS 2009, Proceedings},
  booktitle = {Frontiers of Combining Systems, 7th International Symposium, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5749},
  year = {2009},
  month = sep,
  address = {Trento, Italy},
  isbn = {978-3-642-04221-8},
  doi = {http://dx.doi.org/10.1007/978-3-642-04222-5},
  type_publi = {icolcomlec},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes}
}