Publications

Cette thèse étudie deux approches pour augmenter la sûreté de fonctionnement des programmes informatiques par analyse statique. La première approche est l'utilisation du typage qui permet de prouver automatiquement qu'un programme s'évalue sans échouer. Le langage fonctionnel ML possède un système de type très riche et un algorithme effectuant une synthèse automatique des types. On s'intéresse à son adaptation aux types algébriques généralisés (GADT). Dans ce cadre, le calcul efficace d'un type plus général est impossible. On propose une stratification du langage qui maintient les caractéristiques habituelles sur le fragment ML et qui isole le traitement des GADT en explicitant leur utilisation. Le langage obtenu, MLGX, nécessite des annotations de type qui alourdissent les programmes. Une seconde strate, MLGI, offre au programmeur un mécanisme de synthèse locale, prédictible et efficace bien qu'incomplet, de la plupart de ces annotations. La première partie s'achève avec une démonstration de l'expressivité des GADT pour coder les invariants des automates à pile utilisés par l'analyse syntaxique LR. La seconde approche augmente le langage par des assertions logiques permettant d'exprimer des spécifications de complexité arbitraire. On vérifie la conformité de la sémantique du programme vis-à-vis de ces spécifications à l'aide d'une technique appelée logique de Hoare et d'outils semi-automatiques de preuves mathématiques sur ordinateur. Les choix de conception du système permettent de traiter les fonctions de première classe. Ils sont dirigés par une implantation qui trouve une illustration dans la certification d'un module d'arbres dénotant des ensembles finis.

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.

The LR parser generators that are bundled with many functional programming language implementations produce code that is untyped, needlessly inefficient, or both. We show that, using generalized algebraic data types, it is possible to produce parsers that are well-typed (so they cannot unexpectedly crash or fail) and nevertheless efficient. This is a pleasing result as well as an illustration of the new expressiveness offered by generalized algebraic data types.

We offer a solution to the type inference problem for an extension of Hindley and Milner's type system with generalized algebraic data types. Our approach is in two strata. The bottom stratum is a core language that marries type inference in the style of Hindley and Milner with type checking for generalized algebraic data types. This results in an extremely simple specification, where case constructs must carry an explicit type annotation and type conversions must be made explicit. The top stratum consists of (two variants of) an independent shape inference algorithm. This algorithm accepts a source term that contains some explicit type information, propagates this information in a local, predictable way, and produces a new source term that carries more explicit type information. It can be viewed as a preprocessor that helps produce some of the type annotations required by the bottom stratum. It is proven sound in the sense that it never inserts annotations that could contradict the type derivation that the programmer has in mind.

DIMI is a tool aimed at developing grapheme-to-phoneme (G2P) transcription systems. It provides the user with a declarative formalism for expressing the transduction of symbolic streams annotated with predicates. This formalism is organised in 3 layers : contextual rules using ex- tended rational expressions express the individual rewriting rules. Rules are organized in strategies, which specify how individual rules should be applied : sequentially, in parallel... Strategies are further organised in modules, al- lowing the user to manage complex rule sets. A modular, complete rule set for French is also presented, which illustrates the various possibilities of this language.

This paper reports on a new software platform called VAUCANSON and dedicated to the computation with automata and transducers. Its main feature is the capacity of dealing with automata whose labels may belong to various algebraic structures.The paper successively describes the main features of the VAUCANSON platform, including the fact that the very rich data structure used to implement automata does not weigh too much on the performance, shows how VAUCANSON allows to program algorithms on automata in a way which is very close to the mathematical expression of the algorithm and finally explains the main choices of the programming design that enable to achieve both genericity and efficiency.

The Vaucanson library works on weighted finite state machines in an alge- braic framework. As computing tools, FSMs must provide efficient services. Yet, abstraction is needed to obtain genericity but also to define properly what objects we are working on. Even if parameterized classes are a known solution to this problem, the different kinds of algorithm specializations are limited when using usual template techniques. This paper describes a new design pattern called E LEMENT which enables the orthogo- nal specialization of generic algorithms w.r.t. the algebraic concept and w.r.t. the implementation. The idea is to make concept and implementation explicitly usable as object instances. First, we show how it solves the specialization problem. Then, we detail its implementation and how we deal with some technical pitfalls.