publis.bib

@article{boldo12jar,
  author = {Sylvie Boldo and Fran\c{c}ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
  title = {{Wave Equation Numerical Resolution:
  a Comprehensive Mechanized Proof of a C Program}},
  journal = {Journal of Automated Reasoning},
  year = {2012},
  optvolume = {},
  optnumber = {},
  optpages = {},
  optmonth = {},
  note = {Accepted for publication. \url{http://hal.inria.fr/hal-00649240/en/}}
}
@inproceedings{bobot12icfem,
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre},
  title = {Separation Predicates: a Taste of Separation Logic in
    First-Order Logic},
  booktitle = {14th International Conference on Formal Ingineering Methods
   (ICFEM)},
  month = {November},
  year = 2012,
  type_publi = {icolcomlec},
  topics = {team},
  abstract = {This paper introduces \emph{separation predicates}, a technique to
  reuse some ideas from separation logic in the framework of program
  verification using a traditional first-order logic.  The purpose is
  to benefit from existing specification languages, verification
  condition generators, and automated theorem provers.
  Separation predicates are automatically derived
  from user-defined inductive predicates.
  We illustrate
  this idea on a non-trivial case study, namely the composite pattern,
  which is specified in C/ACSL and verified in a fully automatic way
  using SMT solvers Alt-Ergo, CVC3, and Z3.}
}
@inproceedings{filliatre12inforum,
  author = {M\'ario Pereira and Jean-Christophe Filli\^atre and
    Sim\~ao Melo de Sousa},
  title = {{ARMY}: a Deductive Verification Platform for {ARM} Programs Using {Why3}},
  month = {September},
  year = 2012,
  type_publi = {icolcomlec},
  topics = {team},
  abstract = {Unstructured (low-level) programs tend to be challenging
    to prove correct, since the control flow is
    arbitrary complex and there are no obvious points in
    the code where to insert logical assertions. In this
    paper, we present a system to formally verify ARM
    programs, based on a flow sequentialization
    methodology and a formalized ARM semantics. This
    system, built upon the why3 verification platform,
    takes an annotated ARM program, turns it into a set
    of purely sequential flow programs, translates these
    programs' instructions into the corresponding
    formalized opcodes and finally calls the Why3 VCGen
    to generate the verification conditions that can
    then be discharged by provers. A prototype has been
    implemented and used to verify several programming
    examples.},
  booktitle = {INForum 2012}
}
@inproceedings{filliatre12compare,
  author = {Jean-Christophe Filli\^atre and Andrei Paskevich and Aaron Stump},
  title = {The 2nd Verified Software Competition: Experience Report},
  booktitle = {COMPARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems},
  year = 2012,
  editor = {Vladimir Klebanov and Sarah Grebing},
  publisher = {EasyChair},
  type_publi = {icolcomlec},
  topics = {team},
  abstract = {We report on the second verified software competition.  It was
  organized by the three authors on a 48 hours period on November
  8--10, 2011. This paper describes the competition, presents the five
  problems that were proposed to the participants, and gives an
  overview of the solutions sent by the 29 teams that entered the
  competition.},
  url = {http://www.lri.fr/~filliatr/pub/compare2012.pdf}
}
@inbook{filliatre12ejcp,
  author = {Jean-Christophe Filli\^atre},
  title = {Course notes EJCP 2012},
  chapter = {V\'erification d\'eductive de programmes avec {Why3}},
  month = {June},
  year = 2012,
  pdf = {http://why3.lri.fr/ejcp-2012/}
}
@misc{filliatre12jfla,
  author = {Jean-Christophe Filli\^atre},
  title = {Vérification déductive de programmes avec {Why3}},
  month = {Janvier},
  year = 2012,
  note = {Cours aux vingt-troisi\`emes Journ\'ees Francophones des Langages Applicatifs},
  url = {http://why3.lri.fr/jfla-2012/}
}
@inproceedings{filliatre12aipa,
  author = {Jean-Christophe Filli\^atre},
  title = {{Combining Interactive and Automated Theorem Proving
in Why3 (invited talk)}},
  booktitle = {{Automation in Proof Assistants 2012}},
  editor = {Keijo Heljanko and Hugo Herbelin},
  month = {April},
  year = 2012,
  address = {Tallinn, Estonia}
}
@inproceedings{mentre12abz,
  author = {David Mentr\'e and Claude
  March\'e and Jean-Christophe Filli\^atre and Masashi Asuka},
  title = {Discharging Proof Obligations from {Atelier~B} using
  Multiple Automated Provers},
  booktitle = {ABZ Conference},
  year = 2012,
  address = {Pisa, Italy},
  month = {June},
  abstract = {We present a method to discharge proof obligations from Atelier~B
  using multiple SMT solvers. It is based on a faithful modeling of
  B's set theory into polymorphic first-order logic. We report on two
  case studies demonstrating a significant improvement in the ratio of
  obligations that are automatically discharged.},
  pdf = {http://www.lri.fr/~filliatr/publis/abz12.pdf}
}
@inproceedings{filliatre12vstte,
  author = {Jean-Christophe Filli\^atre},
  title = {Verifying Two Lines of {C} with {Why3}: an Exercise in Program Verification},
  booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE)},
  month = {January},
  year = 2012,
  address = {Philadelphia, USA},
  url = {http://why3.lri.fr/queens/queens.pdf},
  abstract = {This article details the formal verification of a 2-line C program
  that computes the number of solutions to the $n$-queens problem.
  The formal proof of (an abstraction of) the C code
  is performed using the Why3 tool to generate
  the verification conditions and several provers (Alt-Ergo, CVC3,
  Coq) to discharge them. The main purpose of this article is to
  illustrate the use of Why3 in verifying an algorithmically complex
  program.}
}
@article{filliatre11sttt,
  author = {Jean-Christophe Filli\^atre},
  title = {Deductive Software Verification},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  month = aug,
  year = 2011,
  publisher = {Springer Berlin / Heidelberg},
  volume = 13,
  number = 5,
  pages = {397-403},
  issn = {1433-2779},
  url = {http://dx.doi.org/10.1007/s10009-011-0211-0},
  doi = {10.1007/s10009-011-0211-0},
  abstract = {Deductive software verification, also known as program proving,
  expresses the correctness of a program as a set
  of mathematical statements, called verification conditions. They are
  then discharged using either automated or interactive theorem
  provers. We briefly review this research area, with an emphasis on
  tools.}
}
@inproceedings{boogie11why3,
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Andrei Paskevich},
  title = {Why3: Shepherd Your Herd of Provers},
  topics = {team},
  booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
  year = 2011,
  address = {Wroc\l{}aw, Poland},
  month = {August},
  url = {http://proval.lri.fr/submissions/boogie11.pdf},
  abstract = {Why3 is the next generation of the
  Why software verification platform. 
  Why3 clearly separates the purely logical
  specification part from generation of verification conditions for programs.
  This article focuses on the former part.
  Why3 comes with a new enhanced language of
  logical specification. It features a rich library of
  proof task transformations that can be chained to produce a suitable
  input for a large set of theorem provers, including SMT solvers,
  TPTP provers, as well as interactive proof assistants.}
}
@inproceedings{filliatre11tfp,
  author = {Jean-Christophe Filli\^atre and K. Kalyanasundaram},
  title = {{Functory: A Distributed Computing Library for Objective Caml}},
  booktitle = {Trends in Functional Programming},
  year = 2011,
  series = {Lecture Notes in Computer Science},
  volume = {7193},
  pages = {65--81},
  topics = {team},
  address = {Madrid, Spain},
  month = {May},
  abstract = {We present Functory, a distributed computing library for
  Objective Caml. The main features of this library
  include (1) a polymorphic API, (2) several implementations to
  adapt to different deployment scenarios such as sequential,
  multi-core or network, and (3) a reliable fault-tolerance mechanism.
  This paper describes the motivation behind this work, as well as
  the design and implementation of the library. It also demonstrates
  the potential of the library using realistic experiments.}
}
@inproceedings{dross11tap,
  author = {Claire Dross and Jean-Christophe Filli\^atre and Yannick Moy},
  title = {{Correct Code Containing Containers}},
  booktitle = {5th International Conference on Tests & Proofs (TAP'11)},
  year = 2011,
  address = {Zurich},
  month = {June},
  topics = {team},
  abstract = {
  For critical software development, containers such as lists, vectors, sets or
  maps are an attractive alternative to ad-hoc data structures based on
  pointers. 
  As standards like DO-178C put formal verification and testing on an equal
  footing, it is important to give users the ability to apply both to the
  verification of code using containers.
  In this paper,
  we present a definition of containers whose aim is to facilitate their
  use in certified software, using modern proof technology and novel
  specification languages. Correct usage of containers and user-provided
  correctness properties can be checked either by execution during testing
  or by formal proof with an automatic prover.
  We present a formal semantics for containers and an axiomatization of this 
  semantics targeted at automatic provers. We have proved in Coq that the
  formal semantics is consistent and that the axiomatization thereof is 
  correct.}
}
@manual{baudin09acsl,
  title = {ACSL: ANSI/ISO C Specification Language, version 1.4},
  author = {Patrick Baudin  and Jean-Christophe Filli\^atre and Claude March\'e and Benjamin Monate and Yannick Moy and Virgile Prevosto},
  year = 2009,
  note = {\url{http://frama-c.cea.fr/acsl.html}},
  url = {http://frama-c.cea.fr/acsl.html}
}
@inproceedings{filliatre11jfla,
  author = {Filli\^atre, Jean-Christophe and Kalyanasundaram, Krishnamani},
  title = {Functory : Une biblioth\`eque de calcul distribu\'e pour {Objective Caml}},
  year = 2011,
  booktitle = {Vingt-deuxi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {La Bresse, France},
  publisher = {INRIA},
  url = {http://www.lri.fr/~filliatr/publis/jfla-2011.pdf},
  abstract = {Cet article présente Functory, une bibliothèque de calcul distribué 
  pour Objective Caml. Les principales caractéristiques de cette
  bibliothèque sont (1) une interface polymorphe, (2) plusieurs
  réalisations correspondant à des contextes d'utilisation différents
  et (3) un mécanisme de tolérance aux pannes.
  Cet article détaille la conception et la réalisation de Functory et
  montre son potentiel sur de nombreux exemples.}
}
@inproceedings{OpenCert2010,
  author = {M. Barbosa and J.-C. Filliâtre and J. Sousa Pinto and B. Vieira},
  title = {{A Deductive Verification Platform for Cryptographic Software}},
  booktitle = {{4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010)}},
  year = 2010,
  address = {Pisa, Italy},
  volume = {33},
  publisher = {Electronic Communications of the EASST},
  url = {http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/461},
  month = {September}
}
@inproceedings{boldo10-itp,
  author = {Sylvie Boldo and François Clément and Jean-Christophe Filliâtre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
  title = {{Formal Proof of a Wave Equation Resolution Scheme: the Method Error}},
  booktitle = {Proceedings of the first Interactive Theorem Proving Conference},
  year = 2010,
  series = {LNCS},
  address = {Edinburgh, Scotland},
  month = jul,
  publisher = {Springer},
  note = {(merge of TPHOL and ACL2)},
  topics = {team},
  url = {http://hal.inria.fr/inria-00450789/en/},
  abstract = {Popular finite difference numerical schemes for the resolution of the
one-dimensional acoustic wave equation are well-known to be convergent.
We present a comprehensive formalization of the simplest scheme and formally
prove its convergence in Coq.
The main difficulties lie in the proper definition of asymptotic behaviors
and the implicit way they are handled in the mathematical pen-and-paper
proofs.
To our knowledge, this is the first time this kind of mathematical proof is
machine-checked.
}
}
@inproceedings{conchon10jfla,
  author = {Conchon, Sylvain and Filli\^atre, Jean-Christophe 
 and Le Fessant, Fabrice and Robert, Julien and Von Tokarski, Guillaume},
  title = {{Observation temps-réel de programmes Caml}},
  topics = {team, lri},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  year = 2010,
  booktitle = {Vingt-et-uni\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Vieux-Port La Ciotat, France},
  publisher = {INRIA},
  abstract = {  Pour mettre au point un programme, tant du point de vue de sa
  correction que de ses performances, il est naturel de chercher à
  observer son exécution. On peut ainsi chercher à observer la gestion
  de la mémoire, le temps passé dans une certaine partie du code, ou
  encore certaines valeurs calculées par le programme.  De nombreux
  outils permettent de telles observations (moniteur système,
  \emph{profiler} ou \emph{debugger} génériques ou spécifiques au
  langage, instrumentation explicite du code, etc.).  Ces outils ne
  proposent cependant que des analyses << après coup >> ou des
  observations très limitées.  Cet article présente Ocamlviz, une
  bibliothèque pour instrumenter du code Ocaml et des outils pour
  visualiser ensuite son exécution, en temps-réel et de manière
  distante.},
  url = {http://www.lri.fr/~conchon/publis/ocamlviz-jfla2010.pdf}
}
@inproceedings{KanigFilliatre09wml,
  author = {Johannes Kanig and Jean-Christophe Filli\^atre},
  title = {{Who: A Verifier for Effectful Higher-order Programs}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Edinburgh, Scotland, UK},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  month = aug,
  year = 2009,
  pdf = {http://www.lri.fr/~filliatr/ftp/publis/wml09.pdf},
  abstract = {We present Who, a tool for verifying effectful higher-order
  functions. It features {\em Effect polymorphism}, higher-order logic
  and the possibility to reason about state in the logic, which enable
  highly modular specifications of generic code. Several small
  examples and a larger case study demonstrate its usefulness. The
  Who~tool is intended to be used as an intermediate language for
  verification tools targeting ML-like programming languages.}
}
@inproceedings{boldo09calculemus,
  author = {Sylvie Boldo and Jean-Christophe Filli\^atre and Guillaume Melquiond},
  title = {Combining {C}oq and {G}appa for {C}ertifying {F}loating-{P}oint
  {P}rograms },
  booktitle = {16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning},
  year = {2009},
  month = jul,
  publisher = {LNCS/LNAI},
  topics = {team},
  url = {http://www.lri.fr/~filliatr/publis/calculemus09.pdf},
  abstract = {  Formal verification of numerical programs is notoriously difficult.
  On the one hand, there exist automatic tools specialized in floating-point
  arithmetic, such as Gappa, but they target very restrictive logics. On
  the other hand, there are interactive theorem provers based on the LCF
  approach, such as Coq,
  that handle a general-purpose logic but that lack proof automation for
  floating-point properties. To alleviate these issues, we have implemented a mechanism
  for calling Gappa from a Coq interactive proof. This paper presents
  this combination and shows on several examples how this approach offers a
  significant speedup in the process of verifying floating-point programs.
}
}
@inproceedings{mlpost09jfla,
  author = {Romain Bardou and Jean-Christophe Filli\^atre and Johannes Kanig and St\'ephane Lescuyer},
  title = {{Faire bonne figure avec Mlpost}},
  booktitle = {{Vingtièmes Journ\'ees Francophones des Langages Applicatifs}},
  year = 2009,
  address = {Saint-Quentin sur Isère},
  publisher = {INRIA},
  url = {http://www.lri.fr/~filliatr/ftp/publis/mlpost-fra.pdf},
  abstract = {Cet article présente Mlpost, une bibliothèque 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éduisante aux langages de macros \LaTeX, aux langages
  spécialisés ou même aux outils graphiques. En particulier,
  l'utilisateur de Mlpost bénéficie de toute l'expressivité
  d'Ocaml et de son typage statique. Enfin Mlpost propose un style
  déclaratif qui diffère de celui, souvent impératif, des outils existants.}
}
@inproceedings{Filliatre08wml,
  author = {Jean-Christophe Filli\^atre},
  title = {{A Functional Implementation of the Garsia--Wachs Algorithm}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  publisher = {ACM},
  year = 2008,
  address = {Victoria, British Columbia, Canada},
  month = {September},
  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}.}
}
@inproceedings{ConchonFilliatre08esop,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Semi-Persistent Data Structures}},
  booktitle = {17th European Symposium on Programming (ESOP'08)},
  year = 2008,
  address = {Budapest, Hungary},
  note = {Short version of~\cite{ConchonFilliatre07spdsrr}},
  url = {http://www.lri.fr/~filliatr/ftp/publis/spds-esop08.pdf},
  abstract = {
  A data structure is said to be \emph{persistent} when any update
  operation returns a new structure without altering the old version.
  This paper introduces a new notion of persistence, called
  \emph{semi-persistence}, where only ancestors of the most recent
  version can be accessed or updated. 
  Making a data structure semi-persistent may
  improve its time and space complexity.  This is of particular
  interest in backtracking algorithms manipulating persistent data
  structures, where this property is usually satisfied.
  We propose a proof system to statically check the valid use of
  semi-persistent data structures. It requires a few annotations from
  the user and then generates proof obligations that are
  automatically discharged by a dedicated decision procedure.}
}
@inproceedings{Filliatre07corde,
  author = {Jean-Christophe Filli\^atre},
  title = {{Gagner en passant \`a la corde}},
  booktitle = {Dix-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
  year = 2008,
  address = {\'Etretat, France},
  publisher = {INRIA},
  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ême 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{Filliatre07mix,
  author = {Jean-Christophe Filli\^atre},
  title = {{Formal Verification of MIX Programs}},
  booktitle = {{Journées en l'honneur de Donald E. Knuth}},
  year = 2007,
  address = {Bordeaux, France},
  month = {October},
  url = {http://www.lri.fr/~filliatr/publis/verifmix.pdf},
  abstract = {We introduce a methodology to formally verify MIX programs.
  It consists in annotating a MIX program with logical annotations
  and then to turn it into a set of purely sequential programs on
  which classical techniques can be applied.
  Contrary to other approaches of verification of unstructured
  programs, we do not impose the location of annotations but only the
  existence of at least one invariant on each cycle in the control
  flow graph. A prototype has been implemented and used to verify
  several programs from \emph{The Art of Computer Programming}.}
}
@techreport{ConchonFilliatre07spdsrr,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Semi-Persistent Data Structures}},
  institution = {{LRI, Universit\'e Paris Sud}},
  type = {{Research Report}},
  number = {1474},
  month = {September},
  year = 2007,
  url = {http://www.lri.fr/~filliatr/ftp/publis/spds-rr.pdf},
  abstract = {  
  A data structure is said to be persistent when any update
  operation returns a new structure without altering the old version.
  This paper introduces a new notion of persistence, called
  semi-persistence, where only ancestors of the most recent
  version can be accessed or updated. 
  Making a data structure semi-persistent may
  improve its time and space complexity.  This is of particular
  interest in backtracking algorithms manipulating persistent data
  structures, where this property is usually satisfied.
  We propose a proof system to statically check the valid use of
  semi-persistent data structures. It requires a few annotations from
  the user and then generates proof obligations that are
  automatically discharged by a dedicated decision procedure.
  Additionally, we give some examples of semi-persistent data
  structures (arrays, lists and hash tables).}
}
@unpublished{Filliatre07queens,
  author = {Jean-Christophe Filli\^atre},
  title = {{Queens on a Chessboard: 
       an Exercise in Program Verification}},
  note = {Unpublished},
  month = {January},
  year = 2007,
  url = {http://why.lri.fr/queens/queens.ps},
  abstract = {  
  This article details the formal verification of a 2-lines C program
  which computes the number of solutions to the $n$-queens problem.
  The formal proof is performed using the Caduceus tool to generate
  the verification conditions and several provers (Simplify, Ergo,
  Coq) to discharge them. The main purpose of this article is to show
  how a complex behavior of a C program can be established with
  \caduceus. The key is here the possibility to introduce an abstract
  model and to relate it to the source code using ghost statements.}
}
@inproceedings{filliatre07cav,
  author = {Jean-Christophe Filli\^atre and Claude March\'e},
  title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
  Verification},
  editor = {Werner Damm and Holger Hermanns},
  booktitle = {19th International Conference on Computer Aided Verification},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  address = {Berlin, Germany},
  month = jul,
  year = {2007},
  url = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf}
}
@inproceedings{BoldoFilliatre07,
  author = {Sylvie Boldo and Jean-Christophe Filli\^atre},
  title = {{Formal Verification of Floating-Point Programs}},
  booktitle = {18th IEEE International Symposium on Computer Arithmetic},
  month = {June},
  year = 2007,
  address = {Montpellier, France},
  url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf},
  abstract = {
  This paper introduces a methodology to perform formal verification
  of floating-point C programs. It extends an existing tool for the
  verification of C programs, Caduceus, with new annotations specific
  to floating-point arithmetic. The Caduceus first-order logic model
  for C programs is extended accordingly. Then verification conditions
  expressing the correctness of the programs are obtained in the usual
  way and can be discharged interactively with the Coq proof
  assistant, using an existing Coq formalization of floating-point
  arithmetic.  This methodology is already implemented and has been
  successfully applied to several short floating-point programs, which
  are presented in this paper.}
}
@inproceedings{ConchonFilliatre07wml,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{A Persistent Union-Find Data Structure}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  publisher = {ACM},
  pages = {37--45},
  year = 2007,
  address = {Freiburg, Germany},
  month = {October},
  note = {English version of \cite{ConchonFilliatre06b}},
  url = {http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
  abstract = {The problem of disjoint sets, also known as union-find, 
  consists in maintaining a partition of a finite set within a data
  structure. This structure provides two operations: a function find
  returning the class of an element and a function union merging two
  classes. An optimal and imperative solution is known since 1975.
  However, the imperative nature of this data structure may be a
  drawback when it is used in a backtracking algorithm. This paper
  details the implementation of a persistent union-find data structure
  as efficient as its imperative counterpart.  To achieve this result,
  our solution makes heavy use of imperative features and thus it is a
  significant example of a data structure whose side effects are
  safely hidden behind a persistent interface.  To strengthen this
  last claim, we also detail a formalization using the Coq proof
  assistant which shows both the correctness of our solution and its
  observational persistence.}
}
@inproceedings{ConchonFilliatre06b,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Union-Find Persistant}},
  booktitle = {Dix-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
  year = 2007,
  address = {Aix-les-bains, France},
  publisher = {INRIA},
  url = {http://www.lri.fr/~filliatr/ftp/publis/puf.pdf},
  abstract = {  
  Le problème des classes disjointes, connu sous le nom de
  \emph{union-find}, consiste à maintenir dans une structure de
  données une partition d'un ensemble fini. Cette structure fournit deux
  opérations : une fonction \emph{find} déterminant la classe d'un
  élément et une fonction \emph{union} réunissant deux classes.  Une
  solution optimale et impérative, due à Tarjan, est connue depuis
  longtemps.

  Cependant, le caractère impératif de cette structure de données
  devient gênant lorsqu'elle est utilisée dans un contexte où
  s'effectuent des retours en arrière (\emph{backtracking}). Nous
  présentons dans cet article une version persistante de
  \emph{union-find} dont la complexité est comparable à celle de la
  solution impérative. Pour obtenir cette efficacité, notre solution
  utilise massivement des traits impératifs. C'est pourquoi nous
  présentons également une preuve formelle de correction, pour
  s'assurer notamment du caractère persistant de cette solution.
}
}
@inproceedings{ConchonFilliatre06,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Type-Safe Modular Hash-Consing}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Portland, Oregon},
  note = {Supersedes~\cite{Filliatre00b}},
  month = {September},
  year = 2006,
  url = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf},
  abstract = {  
  Hash-consing is a technique to share values that are structurally
  equal. Beyond the obvious advantage of saving memory blocks,
  hash-consing may also be used to speedup fundamental operations and
  data structures by several orders of magnitude when sharing is
  maximal.  This paper introduces an Ocaml hash-consing library that
  encapsulates hash-consed terms in an abstract datatype, thus safely
  ensuring maximal sharing. This library is also parameterized by an
  equality that allows the user to identify terms according to an
  arbitrary equivalence relation.}
}
@incollection{conchon07tfpbook,
  author = {Sylvain Conchon and  
     Jean-Christophe Filli\^atre and 
     Julien Signoles},
  title = {{Designing a Generic Graph Library using ML Functors}},
  booktitle = {Trends in Functional Programming},
  publisher = {Intellect},
  year = 2007,
  volume = 8,
  topics = {team, lri},
  type_publi = {irevcomlec}
}
@inproceedings{ocamlgraphTFP07,
  author = {Sylvain Conchon and  
     Jean-Christophe Filli\^atre and 
     Julien Signoles},
  title = {{Designing a Generic Graph Library using ML Functors}},
  booktitle = {The Eighth Symposium on Trends in Functional Programming},
  publisher = {Seton Hall University},
  volume = {TR-SHU-CS-2007-04-1},
  pages = {XII/1--13},
  year = 2007,
  address = {New York, USA},
  month = apr,
  topics = {team, lri},
  type_publi = {icolcomlec},
  abstract = {  
  This paper details the design and implementation of Ocamlgraph A
  highly generic graph library for the programming language \ocaml.
  This library features a large set of graph data
  structures---directed or undirected, with or without labels on
  vertices and edges, as persistent or mutable data structures,
  etc.---and a large set of graph algorithms.  Algorithms are written
  independently from graph data structures, which allows combining
  user data structure (resp. algorithm) with Ocamlgraph algorithm
  (resp. data structure).  Genericity is obtained through massive use
  of the Ocaml module system and its functions, the so-called
  functors.},
  url = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp07.ps}
}
@unpublished{AyacheFilliatre06,
  author = {Nicolas Ayache and Jean-Christophe Filli\^atre},
  title = {{Combining the Coq Proof Assistant with First-Order Decision Procedures}},
  note = {Unpublished},
  month = {March},
  year = 2006,
  url = {http://www.lri.fr/~filliatr/publis/coq-dp.ps},
  abstract = {
  We present an integration of first-order automatic theorem provers
  into the Coq proof assistant. This integration is based on a
  translation from the higher-order logic of Coq, the Calculus of
  Inductive Constructions, to a polymorphic first-order logic. This
  translation is defined and proved sound in this paper. It includes
  not only the translation of terms and predicates belonging to the
  first-order fragment, but also several techniques to go well
  beyond: abstractions of higher-order sub-terms, case-analysis,
  mutually recursive functions and inductive types.
  This process has been implemented in the Coq proof assistant to call
  the decision procedures Simplify, CVC Lite, haRVey and Zenon through
  Coq tactics. The first experiments are promising.}
}
@inproceedings{Filliatre06,
  author = {Jean-Christophe Filli\^atre},
  title = {{Backtracking iterators}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Portland, Oregon},
  note = {{Also LRI Research Report 1428}},
  month = sep,
  year = {2006},
  note = {English translation of \cite{Filliatre05}.},
  url = {http://www.lri.fr/~filliatr/publis/enum2.pdf},
  abstract = {
  Iterating over the elements of an abstract collection is usually
  done in ML using a fold-like higher-order function provided by the
  data structure. This article discusses a different paradigm of
  iteration based on purely functional, immutable cursors.  Contrary
  to fold-like iterators, the iteration can be cleanly interrupted at
  any step. Contrary to imperative cursors (such as those found in C++
  and Java libraries) it is possible to backtrack the iterator to a
  previous step.  Several ways to iterate over binary trees are
  examined and close links with G\'erard Huet's Zipper are
  established. Incidentally, we show the well-known two-lists
  implementation of functional queues arising from a Zipper-based
  breadth-first traversal.}
}
@proceedings{Types2004,
  title = {{Types for Proofs and Programs
International Workshop, TYPES 2004}},
  year = 2006,
  editor = {Jean-Christophe Filli\^atre and Christine Paulin-Mohring and Benjamin Werner},
  volume = 3839,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag}
}
@inproceedings{Filliatre05,
  author = {Jean-Christophe Filli\^atre},
  title = {{Itérer avec persistance}},
  booktitle = {Dix-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
  year = 2006,
  address = {Pauillac, France},
  publisher = {INRIA},
  url = {http://www.lri.fr/~filliatr/publis/enum.ps},
  abstract = {
  L'énumération des éléments d'une structure de données est
  généralement réalisée en ML par l'intermédiaire d'une fonction
  d'ordre supérieur. Cet article présente une alternative, sous la
  forme d'itérateurs pas à pas, à l'instar de ce qui se fait en
  programmation orientée objets, mais basés sur des structures
  persistantes, de manière à permettre notamment un éventuel
  \emph{backtracking}. Plusieurs façons de parcourir les arbres
  binaires sont examinées, et des liens étroits avec le Zipper de
  Gérard Huet sont établis.}
}
@misc{TypesSummerSchool2005,
  author = {Jean-Christophe Filli\^atre},
  title = {{Program Verification using Coq. Introduction to the WHY tool}},
  year = 2005,
  note = {Lecture Notes, TYPES Summer School 2005 (Göteborg, Sweden)},
  month = aug,
  url = {http://www.lri.fr/~filliatr/publis/tss-2005.ps.gz}
}
@misc{ipf,
  author = {Jean-Christophe Filli\^atre},
  title = {{Introduction à la programmation fonctionnelle}},
  year = 2004,
  note = {Notes de cours de Master M1},
  url = {http://www.lri.fr/~filliatr/publis/ipf.ps.gz}
}
@inproceedings{ConchonFilliatreSignoles05,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles},
  title = {Le foncteur sonne toujours deux fois},
  booktitle = {Seizi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = mar,
  year = 2005,
  publisher = {INRIA},
  pages = {79--94},
  url = {http://www.lri.fr/~filliatr/ftp/publis/jfla05.ps.gz},
  abstract = {  Cet article présente Ocamlgraph, une bibliothèque générique de graphes pour
  le langage de programmation Ocaml. L'originalité de cette
  bibliothèque est de proposer d'une part un grand nombre de
  structures de données différentes pour représenter les graphes ---
  graphes orientés ou non, structures persistantes ou modifiées en
  place, sommets et arcs avec ou sans étiquettes, marques sur les
  sommets, etc. --- et d'autre part des algorithmes sur les graphes
  écrits indépendamment de la structure de données représentant les
  graphes. Le codage de ces deux aspects originaux a été rendu
  possible par une utilisation massive du système de modules d'Ocaml
  et notamment de ses fonctions, les foncteurs.
}
}
@inproceedings{FilliatreMarche04,
  author = {Jean-Christophe Filli\^atre and Claude March\'e},
  title = {{Multi-Prover Verification of C Programs}},
  booktitle = {Sixth International Conference on
   Formal Engineering Methods (ICFEM)},
  year = 2004,
  address = {Seattle},
  month = nov,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = 3308,
  pages = {15--29},
  url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus.ps.gz},
  abstract = {
  Our goal is the verification of C programs at the source code level
  using formal proof tools. Programs are specified using annotations such
  as pre- and postconditions and global invariants. An
  original approach is presented which allows to formally prove that a
  function implementation satisfies its specification and is free of
  null pointer dereferencing and out-of-bounds array access. 
  The method is not bound to a particular back-end theorem prover.  A
  significant part of the ANSI C language is supported, including
  pointer arithmetic and possible pointer aliasing.  We describe a
  prototype tool and give some experimental results.}
}
@inproceedings{FilliatreLetouzey03,
  author = {J.-C. Filli\^atre and P. Letouzey},
  title = {{Functors for Proofs and Programs}},
  booktitle = {Proceedings of The European Symposium on Programming},
  year = 2004,
  address = {Barcelona, Spain},
  month = {April},
  series = {Lecture Notes in Computer Science},
  volume = 2986,
  pages = {370--384},
  url = {http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz},
  abstract = {
  This paper presents the formal verification with the Coq proof assistant of
  several applicative data structures implementing finite sets. 
  These implementations are parameterized by an ordered type for the
  elements, using functors from the ML module system. The verification
  follows closely this scheme, using the newly Coq module system.
  One of the verified implementation is the actual code for sets and
  maps from the Objective Caml standard library. 
  The formalization refines the informal specifications of these
  libraries into formal ones. The process of
  verification exhibited two small errors in the balancing scheme,
  which have been fixed and then verified.
  Beyond these verification results, this article illustrates the use
  and benefits of modules and functors in a logical framework.
}
}
@techreport{Filliatre03,
  author = {J.-C. Filli\^atre},
  title = {{Why: a multi-language multi-prover verification tool}},
  institution = {{LRI, Universit\'e Paris Sud}},
  type = {{Research Report}},
  number = {1366},
  month = {March},
  year = 2003,
  url = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}
}
@article{FilliatrePottier02,
  author = {J.-C. Filli{\^a}tre and F. Pottier},
  title = {{Producing All Ideals of a Forest, Functionally}},
  journal = {Journal of Functional Programming},
  volume = 13,
  number = 5,
  pages = {945--956},
  month = {September},
  year = 2003,
  url = {http://www.lri.fr/~filliatr/ftp/publis/kr-fp.ps.gz},
  abstract = {
  We present a functional implementation of Koda and Ruskey's
  algorithm for generating all ideals of a forest poset as a Gray
  code. Using a continuation-based approach, we give an extremely
  concise formulation of the algorithm's core. Then, in a number of
  steps, we derive a first-order version whose efficiency is
  comparable to a C implementation given by Knuth.}
}
@unpublished{FORS01,
  author = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar},
  title = {Deciding Propositional Combinations of Equalities and Inequalities},
  note = {Unpublished},
  month = oct,
  year = 2001,
  url = {http://www.lri.fr/~filliatr/ftp/publis/ics.ps},
  abstract = { 
  We address the problem of combining individual decision procedures
  into a single decision procedure.  Our combination approach is based
  on using the canonizer obtained from Shostak's combination algorithm
  for equality.  We illustrate our approach with a combination
  algorithm for equality, disequality, arithmetic inequality, and
  propositional logic.  Unlike the Nelson--Oppen combination where the
  processing of equalities is distributed across different closed
  decision procedures, our combination involves the centralized
  processing of equalities in a single procedure.  The termination
  argument for the combination is based on that for Shostak's
  algorithm.  We also give soundness and completeness arguments.}
}
@inproceedings{ICS,
  author = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar},
  title = {{ICS: Integrated Canonization and Solving (Tool presentation)}},
  booktitle = {Proceedings of CAV'2001},
  editor = {G. Berry and H. Comon and A. Finkel},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = 2102,
  pages = {246--249},
  year = 2001
}
@inproceedings{Filliatre01a,
  author = {J.-C. Filli\^atre},
  title = {La supériorité de l'ordre supérieur},
  booktitle = {Journées Francophones des Langages Applicatifs},
  pages = {15--26},
  month = {Janvier},
  year = 2002,
  address = {Anglet, France},
  url = {http://www.lri.fr/~filliatr/ftp/publis/sos.ps.gz},
  code = {http://www.lri.fr/~filliatr/ftp/ocaml/misc/koda-ruskey.ps},
  abstract = {
  Nous présentons ici une écriture fonctionnelle de l'algorithme de
  Koda-Ruskey, un algorithme pour engendrer une large famille
  de codes de Gray. En s'inspirant de techniques de programmation par
  continuation, nous aboutissons à un code de neuf lignes seulement,
  bien plus élégant que les implantations purement impératives
  proposées jusqu'ici, notamment par Knuth. Dans un second temps,
  nous montrons comment notre code peut être légèrement modifié pour
  aboutir à une version de complexité optimale.
  Notre implantation en Objective Caml rivalise d'efficacité avec les
  meilleurs codes C. Nous détaillons les calculs de complexité,
  un exercice intéressant en présence d'ordre supérieur et d'effets de
  bord combinés.}
}
@techreport{Filliatre00c,
  author = {J.-C. Filli\^atre},
  title = {{Design of a proof assistant: Coq version 7}},
  institution = {{LRI, Universit\'e Paris Sud}},
  type = {{Research Report}},
  number = {1369},
  month = {October},
  year = 2000,
  url = {http://www.lri.fr/~filliatr/ftp/publis/coqv7.ps.gz},
  abstract = {
  We present the design and implementation of the new version of the
  Coq proof assistant. The main novelty is the isolation of the
  critical part of the system, which consists in a type checker for
  the Calculus of Inductive Constructions. This kernel is now
  completely independent of the rest of the system and has been
  rewritten in a purely functional way. This leads to greater clarity
  and safety, without compromising efficiency. It also opens the way to
  the ``bootstrap'' of the Coq system, where the kernel will be
  certified using Coq itself.}
}
@techreport{Filliatre00b,
  author = {J.-C. Filli\^atre},
  title = {{Hash consing in an ML framework}},
  institution = {{LRI, Universit\'e Paris Sud}},
  type = {{Research Report}},
  number = {1368},
  month = {September},
  year = 2000,
  url = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing.ps.gz},
  abstract = {
  Hash consing is a technique to share values that are structurally
  equal. Beyond the obvious advantage of saving memory blocks, hash
  consing may also be used to gain speed in several operations (like
  equality test) and data structures (like sets or maps) when sharing is
  maximal. However, physical adresses cannot be used directly for this
  purpose when the garbage collector is likely to move blocks
  underneath. We present an easy solution in such a framework, with
  many practical benefits.}
}
@misc{ocamlweb,
  author = {J.-C. Filli\^atre and C. March\'e},
  title = {{ocamlweb, a literate programming tool for Objective Caml}},
  note = {Available at \url{http://www.lri.fr/~filliatr/ocamlweb/}},
  url = {http://www.lri.fr/~filliatr/ocamlweb/}
}
@article{Filliatre00a,
  author = {J.-C. Filli\^atre},
  title = {{Verification of Non-Functional Programs 
                   using Interpretations in Type Theory}},
  journal = {Journal of Functional Programming},
  volume = 13,
  number = 4,
  pages = {709--745},
  month = {July},
  year = 2003,
  note = {English translation of~\cite{Filliatre99}.},
  url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz},
  abstract = {We study the problem of certifying programs combining imperative and
  functional features within the general framework of type theory.
  
  Type theory constitutes a powerful specification language, which is
  naturally suited for the proof of purely functional programs. To
  deal with imperative programs, we propose a logical interpretation
  of an annotated program as a partial proof of its specification. The
  construction of the corresponding partial proof term is based on a
  static analysis of the effects of the program, and on the use of
  monads. The usual notion of monads is refined in order to account
  for the notion of effect. The missing subterms in the partial proof
  term are seen as proof obligations, whose actual proofs are left to
  the user. We show that the validity of those proof obligations
  implies the total correctness of the program.
  We also establish a result of partial completeness.
  
  This work has been implemented in the Coq proof assistant.
  It appears as a tactic taking an annotated program as argument and
  generating a set of proof obligations. Several nontrivial
  algorithms have been certified using this tactic.}
}
@article{Filliatre99c,
  author = {J.-C. Filli\^atre},
  title = {{Formal Proof of a Program: Find}},
  journal = {Science of Computer Programming},
  year = 2006,
  volume = 64,
  pages = {332--240},
  doi = {10.1016/j.scico.2006.10.002},
  url = {http://www.lri.fr/~filliatr/ftp/publis/find.ps},
  abstract = {In 1971, C.~A.~R.~Hoare gave the proof of correctness and termination of a
  rather complex algorithm, in a paper entitled \emph{Proof of a
    program: Find}. It is a hand-made proof, where the
  program is given together with its formal specification and where
  each step is fully 
  justified by a mathematical reasoning.  We present here a formal
  proof of the same program in the system Coq, using the
  recent tactic of the system developed to establishing the total
  correctness of 
  imperative programs. We follow Hoare's paper as close as
  possible, keeping the same program and the same specification. We
  show that we get exactly the same proof obligations, which are
  proved in a straightforward way, following the original paper.
  We also explain how more informal reasonings of Hoare's proof are
  formalized in the system Coq.
  This demonstrates the adequacy of the system Coq in the
  process of certifying imperative programs.}
}
@techreport{Filliatre99b,
  author = {J.-C. Filli\^atre},
  title = {{A theory of monads parameterized by effects}},
  institution = {{LRI, Universit\'e Paris Sud}},
  type = {{Research Report}},
  number = {1367},
  month = {November},
  year = 1999,
  url = {http://www.lri.fr/~filliatr/ftp/publis/monads.ps.gz},
  abstract = {Monads were introduced in computer science to express the semantics
  of programs with computational effects, while type and effect
  inference was introduced to mark out those effects.
  In this article, we propose a combination of the notions of effects
  and monads, where the monadic operators are parameterized by effects.
  We establish some relationships between those generalized monads and
  the classical ones.
  Then we use a generalized monad to translate imperative programs
  into purely functional ones. We establish the correctness of that
  translation. This work has been put into practice in the Coq proof
  assistant to establish the correctness of imperative programs.}
}
@phdthesis{Filliatre99,
  author = {J.-C. Filli\^atre},
  title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
  type = {Th{\`e}se de Doctorat},
  school = {Universit\'e Paris-Sud},
  year = 1999,
  month = {July},
  url = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz},
  abstract = {Nous étudions le problème de la certification de programmes mêlant
  traits impératifs et fonctionnels dans le cadre de la théorie des
  types.

  La théorie des types constitue un puissant langage de spécification,
  naturellement adapté à la preuve de programmes purement
  fonctionnels.  Pour y certifier également des programmes impératifs,
  nous commençons par exprimer leur sémantique de manière purement
  fonctionnelle. Cette traduction repose sur une analyse statique des
  effets de bord des programmes, et sur l'utilisation de la notion de
  monade, notion que nous raffinons en l'associant à la notion d'effet
  de manière générale.  Nous montrons que cette traduction est
  sémantiquement correcte.

  Puis, à partir d'un programme annoté, nous construisons une preuve
  de sa spécification, traduite de manière fonctionnelle. Cette preuve
  est bâtie sur la traduction fonctionnelle précédemment
  introduite. Elle est presque toujours incomplète, les parties
  manquantes étant autant d'obligations de preuve qui seront laissées
  à la charge de l'utilisateur.  Nous montrons que la validité de ces
  obligations entraîne la correction totale du programme.

  Nous avons implanté notre travail dans l'assistant de preuve
  Coq, avec lequel il est dès à présent distribué. Cette
  implantation se présente sous la forme d'une tactique prenant en
  argument un programme annoté et engendrant les obligations de
  preuve.  Plusieurs algorithmes non triviaux ont été certifiés à
  l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de
  Knuth-Morris-Pratt).}
}
@inproceedings{FilliatreMagaud99,
  author = {J.-C. Filli\^atre and N. Magaud},
  title = {{Certification of sorting algorithms in the system Coq}},
  booktitle = {Theorem Proving in Higher Order Logics: 
                  Emerging Trends},
  year = 1999,
  abstract = {We present the formal proofs of total correctness of three sorting
  algorithms in the system Coq, namely \textit{insertion sort},
  \textit{quicksort} and \textit{heapsort}. The implementations are
  imperative programs working in-place on a given array. Those
  developments demonstrate the usefulness of inductive types and higher-order
  logic in the process of software certification. They also
  show that the proof of rather complex algorithms may be done in a
  small amount of time --- only a few days for each development ---
  and without great difficulty.},
  url = {http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}
}
@inproceedings{Filliatre98,
  author = {J.-C. Filli\^atre},
  title = {{Proof of Imperative Programs in Type Theory}},
  booktitle = {International Workshop, TYPES '98, Kloster Irsee, Germany},
  publisher = {Springer-Verlag},
  volume = 1657,
  series = {Lecture Notes in Computer Science},
  month = mar,
  year = {1998},
  abstract = {We present a new approach to certifying imperative programs,
  in the context of Type Theory.
  The key is a functional translation of imperative programs, which is
  made possible by an analysis of their effects.
  On sequential imperative programs, we get the same proof
  obligations as those given by Floyd-Hoare logic,
  but our approach also includes functional constructions.
  As a side-effect, we propose a way to eradicate the use of auxiliary
  variables in specifications.
  This work has been implemented in the Coq Proof Assistant and applied
  on non-trivial examples.},
  url = {http://www.lri.fr/~filliatr/ftp/publis/types98.ps.gz}
}
@techreport{Filliatre97,
  author = {J.-C. Filli\^atre},
  institution = {LIP - ENS Lyon},
  number = {97--04},
  title = {{Finite Automata Theory in Coq: 
                              A constructive proof of Kleene's theorem}},
  type = {Research Report},
  month = {February},
  year = {1997},
  abstract = {We describe here a development in the system Coq
  of a piece of Finite Automata Theory. The main result is the Kleene's
  theorem, expressing that regular expressions and finite automata
  define the same languages. From a constructive proof of this result,
  we automatically obtain a functional program that compiles any
  regular expression into a finite automata, which constitutes the main
  part of the implementation of {\tt grep}-like programs. This
  functional program is obtained by the automatic method of {\em
  extraction} which removes the logical parts of the proof to keep only
  its informative contents.  Starting with an idea of what we would
  have written in ML, we write the specification and do the proofs in
  such a way that we obtain the expected program, which is therefore
  efficient.},
  url = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR97/RR97-04.ps.Z}
}
@techreport{Filliatre95,
  author = {J.-C. Filli\^atre},
  institution = {LIP - ENS Lyon},
  number = {96--25},
  title = {{A decision procedure for Direct Predicate
                              Calculus: study and implementation in
                              the Coq system}},
  type = {Research Report},
  month = {February},
  year = {1995},
  abstract = {The paper of J. Ketonen and R. Weyhrauch \emph{A
  decidable fragment of Predicate Calculus} defines a decidable
  fragment of first-order predicate logic - Direct Predicate Calculus
  - as the subset which is provable in Gentzen sequent calculus
  without the contraction rule, and gives an effective decision
  procedure for it. This report is a detailed study of this
  procedure. We extend the decidability to non-prenex formulas. We
  prove that the intuitionnistic fragment is still decidable, with a
  refinement of the same procedure. An intuitionnistic version has
  been implemented in the Coq system using a translation into
  natural deduction.},
  url = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR96/RR96-25.ps.Z}
}
@techreport{Filliatre94,
  author = {J.-C. Filli\^atre},
  month = {Juillet},
  institution = {Ecole Normale Sup\'erieure},
  title = {{Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct~: \'etude et impl\'ementation dans le syst\`eme Coq}},
  type = {Rapport de {DEA}},
  year = {1994},
  url = {ftp://ftp.lri.fr/LRI/articles/filliatr/memoire.dvi.gz}
}
@techreport{CourantFilliatre93,
  author = {J. Courant et J.-C. Filli\^atre},
  month = {Septembre},
  institution = {Ecole Normale Sup\'erieure},
  title = {{Formalisation de la th\'eorie des langages 
                              formels en Coq}},
  type = {Rapport de ma\^{\i}trise},
  year = {1993},
  url = {http://www.ens-lyon.fr/~jcourant/stage_maitrise.dvi.gz},
  url2 = {http://www.ens-lyon.fr/~jcourant/stage_maitrise.ps.gz}
}