2008-conference.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2008-conference.cite -ob 2008-conference.bib -c 'year = 2008 and topics : "team" and $type="inproceedings"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../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 = {https://usr.lmf.cnrs.fr/~jcf/publis/gw-wml08.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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},
hal = {https://inria.hal.science/hal-04045849},
doi = {10.1007/978-3-540-78739-6_25},
title = {Semi-Persistent Data Structures},
crossref = {esop08},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/spds-rr.pdf},
x-url = {https://usr.lmf.cnrs.fr/~jcf/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 = {https://usr.lmf.cnrs.fr/~jcf/publis/cordes.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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
}