2008-conference.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc 2008-conference.cite -ob 2008-conference.bib -c 'year = 2008 and topics : "team" and $type="inproceedings"' /home/marche/biblio/abbrevs.bib /home/marche/biblio/demons.bib /home/marche/biblio/demons2.bib /home/marche/biblio/demons3.bib /home/marche/biblio/team.bib /home/marche/biblio/crossrefs.bib}}
@inproceedings{castagna08icfp,
  author = {Giuseppe Castagna and Kim Nguyen},
  title = {Typed iterators for {XML}},
  booktitle = {ICFP},
  year = {2008},
  pages = {15--26},
  ee = {http://doi.acm.org/10.1145/1411204.1411210},
  crossref = {icfp08},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  topics = {team}
}
@inproceedings{benzaken08ppdp,
  author = {V. Benzaken and G.Castagna and D. Colazzo and C. Miachon},
  title = {Pattern by Example: Type-driven Visual Programming of {XML} Queries".},
  booktitle = {10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming},
  year = 2008,
  address = {Valencia, Spain},
  month = {July},
  publisher = {ACM Press},
  topics = {team, lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {PPDP},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@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{Filliatre08wml,
  author = {Jean-Christophe Filli\^atre},
  title = {{A Functional Implementation of the Garsia--Wachs Algorithm}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  publisher = {ACM Press},
  year = 2008,
  address = {Victoria, British Columbia, Canada},
  month = {September},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-pdf = {http://www.lri.fr/~filliatr/publis/gw-wml08.pdf},
  url = {http://www.lri.fr/~filliatr/publis/gw-wml08.pdf},
  abstract = {  This functional pearl proposes an ML implementation of
  the Garsia--Wachs algorithm.
  This somewhat obscure algorithm builds a binary tree with minimum
  weighted path length from weighted leaf nodes given in symmetric
  order. Our solution exhibits the usual benefits of functional
  programming (use of immutable data structures, pattern-matching,
  polymorphism) and nicely compares to the purely imperative
  implementation from \emph{The Art of Computer Programming}.},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ML}
}
@inproceedings{ConchonFilliatre08esop,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Semi-Persistent Data Structures}},
  crossref = {esop08},
  year = 2008,
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/spds-rr.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/spds-rr.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ESOP},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@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}
}
@inproceedings{Filliatre07corde,
  author = {Jean-Christophe Filli\^atre},
  title = {{Gagner en passant \`a la corde}},
  year = 2008,
  topics = {team, lri},
  type_publi = {colcomlec},
  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},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/cordes.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/cordes.pdf},
  abstract = {
  Cet article pr\'esente une r\'ealisation en Ocaml de la structure de
  cordes introduite par Boehm, Atkinson et Plass. Nous montrons
  notamment comment cette structure de donn\'ees s'\'ecrit naturellement
  comme un foncteur, transformant une structure de s\'equence en une
  autre structure de m\^eme interface. Cette fonctorisation a de
  nombreuses applications au-del\`a de l'article original. Nous en
  donnons plusieurs, dont un \'editeur de texte dont les performances
  sur de tr\`es gros fichiers sont bien meilleures que celles des
  \'editeurs les plus populaires.}
}
@inproceedings{MandelMaranget08esop,
  author = {Louis Mandel and Luc Maranget},
  title = {Programming in {JoCaml} (Tool Demonstration)},
  crossref = {esop08},
  year = 2008,
  pages = {108--111},
  x-pdf = {http://www.lri.fr/~mandel/papers/MandelMaranget-ESOP-2008.pdf},
  url = {http://www.lri.fr/~mandel/papers/MandelMaranget-ESOP-2008.pdf},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ESOP},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{filliatre08smt,
  author = {Jean-Christophe Filli\^atre},
  title = {{Using SMT solvers for deductive verification of C and Java programs}},
  booktitle = {{SMT 2008: 6th International Workshop on Satisfiability Modulo}},
  editor = {Clark Barrett and Leonardo de Moura},
  year = 2008,
  topics = { team},
  type_digiteo = {conf_isbn},
  type_publi = {colloque},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-invited-conference = {yes},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-support = {actes_aux},
  x-cle-support = {SMT},
  address = {Princeton, USA}
}
@inproceedings{Pouzet08c,
  author = {Albert Cohen and Louis Mandel and Florence Plateau and
                  Marc Pouzet},
  title = {{Abstraction of Clocks in Synchronous Data-flow Systems}},
  booktitle = {The Sixth ASIAN Symposium on Programming Languages and Systems
              (APLAS)},
  abstract = { Synchronous data-flow languages such as Lustre manage infinite
  sequences or streams as basic values. Each stream is
  associated to a clock which defines the instants where the
  current value of the stream is present. This clock is a type
  information and a dedicated type system --- the so-called
  clock-calculus --- statically rejects programs which cannot be
  executed synchronously. In existing synchronous languages, it
  amounts at asking whether two streams have the same clocks and thus
  relies on clock equality only. Recent works have shown the interest
  of introducing some relaxed notion of synchrony, where two streams can
  be composed as soon as they can be synchronized through the
  introduction of a finite buffer (as done in the SDF model of Edward
  Lee).  This technically consists in replacing typing by
  subtyping. The present paper introduces a simple way to achieve
  this relaxed model through the use of clock
    envelopes. These clock envelopes are sets of concrete clocks which
  are not necessarily periodic. This allows to model various features
  in real-time embedded software such as bounded jitter as found in
  video-systems,  execution time of real-time processes and
  scheduling resources or the communication through buffers. We
  present the algebra of clock envelopes and its main theoretical
  properties.},
  x-pdf = {http://www.lri.fr/~plateau/papers/aplas08.pdf},
  url = {http://www.lri.fr/~plateau/papers/aplas08.pdf},
  year = 2008,
  month = dec,
  date = {9--11},
  series = {Lecture Notes in Computer Science},
  volume = {5356},
  pages = {237--254},
  address = {Bangalore, India},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {APLAS},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  topics = {team}
}
@inproceedings{Pouzet08b,
  author = {Gwenael Delaval and Alain Girault and Marc Pouzet},
  title = {{A Type System for the Automatic Distribution
                   of Higher-order Synchronous Dataflow Programs}},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems
                  (LCTES)},
  year = 2008,
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LCTES},
  address = {Tucson, Arizona},
  month = jun,
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  topics = {team}
}
@inproceedings{Pouzet08a,
  author = {Dariusz Biernacki and Jean-Louis Cola\c{c}o and Gr\'egoire Hamon
                  and Marc Pouzet},
  title = {{Clock-directed Modular Code Generation of Synchronous Data-flow
                   Languages}},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems
                  (LCTES)},
  year = 2008,
  address = {Tucson, Arizona},
  month = jun,
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {LCTES},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  topics = {team}
}
@inproceedings{MandelPlateau2008SLAP,
  author = {Louis Mandel and Florence Plateau},
  title = {Interactive Programming of Reactive Systems},
  booktitle = {Proceedings of Model-driven High-level Programming of Embedded Systems ({SLA++P'08})},
  year = 2008,
  month = apr,
  address = {Budapest, Hungary},
  pages = {44--59},
  x-pdf = {http://www.lri.fr/~mandel/papers/MandelPlateau-SLAP-2008.pdf},
  url = {http://www.lri.fr/~mandel/papers/MandelPlateau-SLAP-2008.pdf},
  topics = {team},
  type_publi = {icolcomlec},
  series = {Electronic Notes in Computer Science},
  publisher = {Elsevier Science Publishers},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ENTCS},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{moy08vmcai,
  author = {Yannick Moy},
  title = {Sufficient Preconditions for Modular Assertion Checking},
  crossref = {vmcai08},
  pages = {188--202},
  x-pdf = {http://www.lri.fr/~moy/publis/moy08vmcai.pdf},
  url = {http://www.lri.fr/~moy/publis/moy08vmcai.pdf},
  topics = {team, lri},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VMCAI},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{sozeau08tphols,
  author = {Matthieu Sozeau and Nicolas Oury},
  crossref = {tphols2008},
  url = {http://www.lri.fr/~sozeau/research/publications/First-Class_Type_Classes.pdf},
  x-slides = {http://www.lri.fr/~sozeau/research/publications/First-Class_Type_Classes-TPHOLs-200808.pdf},
  title = {{F}irst-{C}lass {T}ype {C}lasses},
  abstract = {
Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for
specifying with abstract structures by quantification on contexts. However,
both systems are limited by second-class implementations of these constructs,
and these limitations are only overcomed by ad-hoc extensions to
the respective systems. We propose an embedding of type classes into a
dependent type theory that is first-class and supports some of the most
popular extensions right away. The implementation is correspondingly
cheap, general and very well integrated inside the system, as we have
experimented in Coq. We show how it can be used to help structured
programming and proving by way of examples.},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {TPHOLs},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{bol08rnc,
  title = {Formal proof for delayed finite field arithmetic using floating point operators},
  author = {Sylvie Boldo and Marc Daumas and Pascal Giorgi},
  booktitle = {Proceedings of the 8th Conference on Real Numbers and
                   Computers},
  year = {2008},
  address = {Santiago de Compostela, Spain},
  month = jul,
  pages = {113--122},
  editor = {Daumas, Marc and Bruguera, Javier},
  x-pdf = {http://hal.archives-ouvertes.fr/docs/00/27/89/89/PDF/rnc.pdf},
  hal = {http://hal.inria.fr/inria-00278989/en/},
  topics = {team,lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {RNC},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{bardou08ftfjp,
  author = {Romain Bardou},
  title = {Ownership, Pointer Arithmetic and Memory Separation},
  crossref = {ftfjp08},
  topics = {team},
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {FTJP},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url = {http://romain.bardou.fr/papers/jcown.pdf}
}
@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{regis-gianas-pottier-08,
  author = {Yann R\'egis-Gianas and Fran\c{c}ois Pottier},
  title = {A {Hoare} Logic for Call-by-Value Functional
                 Programs},
  year = {2008},
  url = {http://cristal.inria.fr/~fpottier/publis/regis-gianas-pottier-hoarefp.pdf},
  doi = {10.1007/978-3-540-70594-9_17},
  pages = {305--335},
  topics = {team},
  abstract = {We present a Hoare logic for a call-by-value
                 programming language equipped with recursive,
                 higher-order functions, algebraic data types, and a
                 polymorphic type system in the style of Hindley and
                 Milner. It is the theoretical basis for a tool that
                 extracts proof obligations out of programs annotated
                 with logical assertions. These proof obligations,
                 expressed in a typed, higher-order logic, are
                 discharged using off-the-shelf automated or interactive
                 theorem provers. Although the technical apparatus that
                 we exploit is by now standard, its application to
                 functional programming languages appears to be new, and
                 (we claim) deserves attention. As a sample application,
                 we check the partial correctness of a balanced binary
                 search tree implementation.},
  booktitle = {Proceedings of the Ninth International Conference on
                 Mathematics of Program Construction (MPC'08)},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {MPC},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@proceedings{tphols2008,
  title = {Theorem Proving in Higher Order Logics:
                           21th International Conference, TPHOLs 2008},
  booktitle = {21th International Conference on Theorem Proving in Higher Order Logics},
  editor = {Otmame A{\"i}t-Mohamed and C\'esar Mu{\~n}oz and Sofi\`ene Tahar},
  series = {Lecture Notes in Computer Science},
  volume = 5170,
  year = 2008,
  addresse = {Montr\'eal, Canada},
  month = aug,
  publisher = {Springer}
}
@proceedings{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{icfp08,
  editor = {James Hook and Peter Thiemann},
  title = {Proceeding of the 13th ACM SIGPLAN international conference
               on Functional programming, ICFP 2008},
  booktitle = {13th ACM SIGPLAN international conference
               on Functional programming, ICFP 2008},
  address = {Victoria, BC, Canada},
  publisher = {ACM},
  year = {2008},
  month = sep,
  isbn = {978-1-59593-919-7}
}
@proceedings{vmcai08,
  editor = {Francesco Logozzo and Doron Peled and Lenore Zuck},
  title = {Verification, Model Checking, and Abstract Interpretation},
  booktitle = {9th International Conference on Verification, Model Checking, and Abstract Interpretation},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 4905,
  address = {San Francisco, California, USA},
  month = jan,
  year = {2008}
}
@proceedings{esop08,
  title = {17th European Symposium on Programming (ESOP'08)},
  booktitle = {17th European Symposium on Programming (ESOP'08)},
  year = 2008,
  address = {Budapest, Hungary},
  month = apr
}
@proceedings{ftfjp08,
  title = {Formal Techniques for Java-like Programs},
  year = 2008,
  booktitle = {Formal Techniques for Java-like Programs (FTfJP'08)},
  address = {Paphos, Cyprus},
  month = jul
}