[21] Albert Cohen, Louis Mandel, Florence Plateau, and Marc Pouzet. Abstraction of Clocks in Synchronous Data-flow Systems. In The Sixth ASIAN Symposium on Programming Languages and Systems (APLAS), Bangalore, India, December 2008. [ bib | PDF | .pdf ]
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.

[20] Jean-Christophe Filliâtre. A Functional Implementation of the Garsia-Wachs Algorithm. In ACM SIGPLAN Workshop on ML, Victoria, British Columbia, Canada, September 2008. ACM. [ bib | PDF | .pdf ]
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 The Art of Computer Programming.

[19] Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. In Otmame Aït-Mohamed, César Muñoz, and Sofiène Tahar, editors, 21th International Conference on Theorem Proving in Higher Order Logics, volume 5170 of Lecture Notes in Computer Science. Springer, August 2008. [ bib | Slides | .pdf ]
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.

[18] Sylvie Boldo, Marc Daumas, and Pascal Giorgi. Formal proof for delayed finite field arithmetic using floating point operators. In Marc Daumas and Javier Bruguera, editors, Proceedings of the 8th Conference on Real Numbers and Computers, pages 113-122, Santiago de Compostela, Spain, July 2008. [ bib | full paper on HAL | PDF ]
[17] Romain Bardou. Ownership, pointer arithmetic and memory separation. In Formal Techniques for Java-like Programs (FTfJP'08), Paphos, Cyprus, July 2008. [ bib | .pdf ]
[16] Gwenael Delaval, Alain Girault, and Marc Pouzet. A Type System for the Automatic Distribution of Higher-order Synchronous Dataflow Programs. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008. [ bib ]
[15] Dariusz Biernacki, Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. Clock-directed Modular Code Generation of Synchronous Data-flow Languages. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008. [ bib ]
[14] Évelyne Contejean and Xavier Urbain. The A3PAT approach. In Workshop on Certified Termination WScT08, Leipzig, Germany, May 2008. [ bib ]
[13] Louis Mandel and Florence Plateau. Interactive programming of reactive systems. In Proceedings of Model-driven High-level Programming of Embedded Systems (SLA++P'08), Electronic Notes in Computer Science, pages 44-59, Budapest, Hungary, April 2008. Elsevier Science Publishers. [ bib | PDF | .pdf ]
[12] Évelyne Contejean. Coccinelle, a Coq library for rewriting. In Types, Torino, Italy, March 2008. [ bib ]
[11] Giuseppe Castagna and Kim Nguyen. Typed iterators for XML. In James Hook and Peter Thiemann, editors, ICFP, pages 15-26, Victoria, BC, Canada, September 2008. ACM. [ bib ]
[10] François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane Lescuyer. Implementing Polymorphism in SMT solvers. In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th International Workshop on Satisfiability Modulo, volume 367 of ACM International Conference Proceedings Series, pages 1-5, 2008. [ bib | DOI | PDF | .pdf | Abstract ]
[9] Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer. CC(X): Semantical combination of congruence closure with solvable theories. In Post-proceedings of the 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), volume 198(2) of Electronic Notes in Computer Science, pages 51-69. Elsevier Science Publishers, 2008. [ bib | DOI ]
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.

[8] Sylvain Conchon, Johannes Kanig, and Stéphane Lescuyer. SAT-MICRO : petit mais costaud ! In Dix-neuvièmes Journées Francophones des Langages Applicatifs, Étretat, France, January 2008. INRIA. [ bib | .ps ]
Le problème SAT, qui consiste `a déterminer si une formule booléenne est satisfaisable, est un des problèmes NP-complets les plus célèbres et aussi un des plus étudiés. Basés initialement sur la procédure DPLL, les SAT-solvers modernes ont connu des progrès spectaculaires ces dix dernières années dans leurs performances, essentiellement grâce à deux optimisations: le retour en arrière non-chronologique et l'apprentissage par analyse des clauses conflits. Nous proposons dans cet article une étude formelle du fonctionnement de ces techniques ainsi qu'une réalisation en Ocaml d'un SAT-solver, baptisé SAT-MICRO, intégrant ces optimisations. Le fonctionnement de SAT-MICRO est décrit par un ensemble de règles d'inférence et la taille de son code, 70 lignes au total, permet d'envisager sa certification complète.

[7] Sylvain Conchon and Jean-Christophe Filliâtre. Semi-Persistent Data Structures. In 17th European Symposium on Programming (ESOP'08), Budapest, Hungary, April 2008. [ bib | PDF | .pdf ]
[6] Jean-Christophe Filliâtre. Gagner en passant à la corde. In Dix-neuvièmes Journées Francophones des Langages Applicatifs, Étretat, France, January 2008. INRIA. [ bib | PDF | .pdf ]
Cet article présente une réalisation en Ocaml de la structure de cordes introduite par Boehm, Atkinson et Plass. Nous montrons notamment comment cette structure de données s'écrit naturellement comme un foncteur, transformant une structure de séquence en une autre structure de même interface. Cette fonctorisation a de nombreuses applications au-delà de l'article original. Nous en donnons plusieurs, dont un éditeur de texte dont les performances sur de très gros fichiers sont bien meilleures que celles des éditeurs les plus populaires.

[5] Louis Mandel and Luc Maranget. Programming in JoCaml (tool demonstration). In 17th European Symposium on Programming (ESOP'08), pages 108-111, Budapest, Hungary, April 2008. [ bib | PDF | .pdf ]
[4] Jean-Christophe Filliâtre. Using SMT solvers for deductive verification of C and Java programs. In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th International Workshop on Satisfiability Modulo, Princeton, USA, 2008. [ bib ]
[3] Yannick Moy. Sufficient preconditions for modular assertion checking. In Francesco Logozzo, Doron Peled, and Lenore Zuck, editors, 9th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 4905 of Lecture Notes in Computer Science, pages 188-202, San Francisco, California, USA, January 2008. Springer. [ bib | PDF | .pdf ]
[2] Stéphane Lescuyer and Sylvain Conchon. A reflexive formalization of a SAT solver in Coq. In Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics, 2008. [ bib ]
[1] Yann Régis-Gianas and François Pottier. A Hoare logic for call-by-value functional programs. In Proceedings of the Ninth International Conference on Mathematics of Program Construction (MPC'08), pages 305-335, 2008. [ bib | DOI | .pdf ]
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.