Lifo - Laboratoire d'Informatique Fondamentale d'orléans Université d'Orléans université d'Orléans ENSI Bourges ENSI Bourges

Lifo > Les séminaires du LIFO

 English Version



Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Tel: +33 (0)2 38 41 70 11
Fax: +33 (0)2 38 41 71 37



Les séminaires du LIFO


Accès par année : 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014

Sauf exception, les séminaires se déroulent le lundi de 14h à 15h, Salle de réunion 1, bâtiment IIIA (voir plan du campus).


15/12/2014 : To Be Announced
Eugenie Foustoucos (Computer Science Department of the Athens University of Business and Economics) Résumé

01/12/2014 : SQL/AA : Privacy-Preserving Query Execution using a Decentralized Architecture and Tamper Resistant Hardware
Benjamin Nguyen (LIFO - INSA Centre Val de Loire) Résumé

17/11/2014 : Proposition de combinaison de systèmes en TAL : annotations partielles et décomposition duale
Joseph Le Roux (Laboratoire d'Informatique de Paris Nord, Université Paris 13) Résumé

03/11/2014 : Décompositions de trigraphes
Antoine Mamcarz (LIFO, Université d'Orléans) Résumé

13/10/2014 : Introduction à la vérification déductive avec Frama-C
Virgile Prevosto (CEA LIST) Résumé

29/09/2014 : Modélisation et implémentation de parallélisme implicite pour les simulations scientifiques basées sur des maillages (Soutenance de thèse)
Hélène Coullon (LIFO, Université d'Orléans) Résumé

04/07/2014 : Challenging machine learning classification tasks
André Carlos Ponce Leon Ferreira de Carvalho (Universidade de São Paulo at São Carlos, Brazil) Résumé
Attention : Ce séminaire aura exceptionnellement lieu un vendredi.

23/06/2014 : A Graph Reduction Machine for Web Service Compositions
Martin A. Musicante (Federal University of Rio Grande do Norte, Department of Computer Science, Natal, Brazil) Résumé

16/06/2014 : Vers la construction à large couverture de la représentation du sens de phrases de langue naturelle
Benoît Crabbé (Université Paris Diderot-Paris 7, INRIA Rocquencourt) Résumé

12/05/2014 : On the Context-Freeness Problem for Vector Addition Systems
Grégoire Sutre (Laboratoire LaBRI - CNRS - Université de Bordeaux ) Résumé

05/05/2014 : Les capitalistes sociaux : les sentiers de la gloire sur Twitter
Nicolas Dugué (LIFO - Université d'Orléans) Résumé

28/04/2014 : A Linear-Time Algorithm for Computing the Prime Decomposition of a Directed Graph With Regard to the Cartesian Product
Christophe Crespelle (LIP - ENS Lyon) Résumé

14/04/2014 : Design de structures d'ARN avec contraintes de séquence : une approche à base de langages formels
Alain Denise (Université Paris Sud) Résumé

14/04/2014 : Vers l'analyse statique de langages fonctionnels par réécriture et automates d'arbres
Thomas Genet (IRISA, Université de Rennes) Résumé
Attention : 2e séminaire de l'après-midi / Débute à 15 h.

07/04/2014 : Mesure de performance des algorithmes de routage pour le HPC
Matthieu Perotin (BULL Extreme Computing R&D, Bruyères-Le-Châtel) Résumé

17/03/2014 : Systèmes multi-agents et culture
Loïs Vanhée (Université Montpellier 2 et Universiteit Utrecht) Résumé

10/03/2014 : Systèmes complexes : des réseaux génétiques à la ségrégation urbaine
Eric Goles (Adolfo Ibáñez University, Santiago, Chili) Résumé
Attention : Le séminaire aura lieu dans la salle de séminaire du bâtiment de mathématiques (MAPMO).

03/03/2014 : Several aspects of probabilistic cellular automata
Damien Regnault (IBISC - Université Evry-Val d'Essonne) Résumé

17/02/2014 : Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components
Arnaud Lanoix (LINA, Université de Nantes) Résumé
Attention : Le titre, l’abstract et les slides seront en anglais, mais l’exposé sera en français.

10/02/2014 : Une vue d'ensemble de l'extraction Coq
Pierre Letouzey (PPS - Université Paris Diderot-Paris 7) Résumé

27/01/2014 : First impressions about the use of an embedded low-power manycore processor for HPC
Marcio Castro (Universidade Federal do Rio Grande do Sul (Brazil)) Résumé

20/01/2014 : Extraction de code fonctionnel à partir de spécifications inductives
Catherine Dubois (ENSIIE) Résumé


Résumés des séminaires


To Be Announced Eugenie Foustoucos, Computer Science Department of the Athens University of Business and Economics

Résumé à venir.


SQL/AA : Privacy-Preserving Query Execution using a Decentralized Architecture and Tamper Resistant Hardware Benjamin Nguyen, LIFO - INSA Centre Val de Loire

Current applications, from complex sensor systems (e.g. quantified self) to online e-markets acquire vast quantities of personal information which usually ends up on central servers. Decentralized architectures, devised to help individuals keep full control of their data, hinder global treatments and queries, impeding the development of services of great interest. This paper promotes the idea of pushing the security to the edges of applications, through the use of secure hardware devices controlling the data at the place of their acquisition. To solve this problem, we propose secure distributed querying protocols based on the use of a tangible physical element of trust, reestablishing the capacity to perform global computations without revealing any sensitive information to central servers. There are two main problems when trying to support SQL in this context: perform joins and perform aggregations. In this presentation, we will detail the subset of SQL groub by queries on a sigle table and show how to secure their execution in the presence of honest-but-curious attackers. Cost models and experiments demonstrate that this approach can scale to nationwide infrastructures.


Proposition de combinaison de systèmes en TAL : annotations partielles et décomposition duale Joseph Le Roux, Laboratoire d'Informatique de Paris Nord, Université Paris 13

La résolution de problèmes en TAL par combinaison de systèmes, la réalisation des fameux systèmes joints, fait désormais partie de la "trousse à outils" classique des chercheurs du domaine. Le fait de résoudre plusieurs tâches de front permet bien souvent de bénéficier d'interactions vertueuses entre les systèmes de résolution qui partagent de l'information et "s'entraident" dans leurs tâches respectives. Ceci donne souvent un avantage à ces méthodes comparées aux approches en cascade, dans lesquelles les systèmes sont chaînés séquentiellement. Dans cet exposé nous développerons une approche qui place la combinaison des solutions de systèmes élémentaires au coeur de la démarche de résolution et qui sera illustrée sur deux tâches, l'analyse syntaxique et l'étiquetage de séquences pour la segmentation des mots composés. L'idée centrale est de produire pour une tâche donnée une combinaison de systèmes "artificielle" dans le sens où cette tâche était traditionnellement résolue par un unique système. Nous produisons plusieurs systèmes similaires (par exemple des analyseurs CFG ou des étiqueteurs CRF), mais qui ne voient pas exactement les mêmes données d'entraînement. Plus précisément, nous entraînons tous les systèmes sur les mêmes corpus, mais certains types d'annotations ne seront disponibles qu'à certains systèmes, de telle sorte que les systèmes auront été effectivement entraînés sur des données différentes. Chaque système est alors considéré comme un "expert" avec une vue partielle du problème, et le but de la combinaison est de mettre d'accord ces experts. Les structures produites par les systèmes pouvant être assez différentes, surtout dans le cas des analyseurs syntaxiques, il est difficile de réaliser cette combinaison par pure programmation dynamique (les sous-calculs ne se partagent pas forcément). Cependant, il doit tout de même exister des points d'accord entre les systèmes pour arriver à un consensus. Nous proposons donc de réaliser cette combinaison en utilisant une méthode issue de l'optimisation combinatoire et de la recherche opérationnelle, la décomposition lagrangienne, qui permet d'intégrer des contraintes d'accord à un problème de recherche de meilleure solution. Nous obtenons alors des algorithmes de combinaison qui procèdent par reparamétrisations successives jusqu'à obtention de solutions compatibles avec chaque système. Expérimentalement, nous montrons que cette méthode est très performante. Pour l'analyse syntaxique, nous obtenons les meilleurs résultats à ce jour sur le "Penn Treebank" (EMNLP 2013). Nous obtenons également des résultats au-dessus de l'état de l'art pour la segmentation en mots composés sur le corpus arboré de Paris 7 (COLING 2014).


Décompositions de trigraphes Antoine Mamcarz, LIFO, Université d'Orléans

Résumé à venir.


Introduction à la vérification déductive avec Frama-C Virgile Prevosto, CEA LIST

Frama-C (http://frama-c.com/) est un atelier d'analyse de code C permettant d'établir de nombreuses propriétés de programme grâce à différents greffons proposant chacun une technique particulière. Outre le langage C, Frama-C peut prendre en entrée des spécifications écrites en ACSL (ANSI/ISO C Specification Language), langage basé sur la notion de contrats de fonction. Après avoir rapidement présenté Frama-C et ses principaux greffons, nous nous concentrerons sur l'un d'entre eux, WP, qui permet de prouver la conformité d'une implantation C vis-à-vis d'une spécification ACSL, à partir de la logique de Hoare et de la génération de plus faibles pré-conditions. Plus précisément, WP génère des obligations de preuve à partir des formules ACSL, qui sont ensuite transmises à des prouveurs automatiques comme Alt-ergo. Si les prouveurs indiquent que toutes les obligations sont vraies, alors l'implantation est conforme à sa spécification. Sinon, il faut soit corriger une des deux en cas de bug avéré, soit aider les prouveurs en ajoutant des clauses ACSL intermédiaires pour obtenir des obligations de preuves plus faciles à montrer par les prouveurs. Cette activité de preuve sera illustrée par différents exemples simples de programmes munis de leur spécification.


Modélisation et implémentation de parallélisme implicite pour les simulations scientifiques basées sur des maillages (Soutenance de thèse) Hélène Coullon, LIFO, Université d'Orléans

Le calcul scientifique parallèle est un domaine en plein essor qui peut permettre d'augmenter la vitesse des longs traitements, de traiter des problèmes de taille plus importante ou encore des problèmes plus précis. Ce domaine permet donc d'aller plus loin dans les calculs scientifiques, d'obtenir des résultats plus pertinents, car plus précis, ou d'étudier des problèmes plus volumineux qu'auparavant. Dans le monde plus particulier de la simulation numérique scientifique, la résolution d'équations aux dérivées partielles (EDP) est un calcul particulièrement demandeur en ressources parallèles. Si les ressources matérielles qui permettent le calcul parallèle sont de plus en plus présentes et disponibles pour les scientifiques, à l'inverse leur utilisation et la programmation parallèle se démocratisent difficilement. Pour cette raison, des modèles de programmation parallèle, des outils de développement et même des langages de programmation parallèle ont vu le jour et visent à simplifier l'utilisation de ces machines. Il est toutefois difficile, dans ce domaine dit du "parallélisme implicite", de trouver le niveau d'abstraction idéal pour les scientifiques, tout en réduisant l'effort de programmation. Ce travail de thèse propose tout d'abord un modèle permettant de mettre en oeuvre des solutions de parallélisme implicite pour les simulations numériques et la résolution d'EDP. Ce modèle est appelé "Structured Implicit Parallelism for scientific SIMulations" (SIPSim), et propose une vision au croisement de plusieurs types d'abstraction, en tentant de conserver leurs avantages. Afin de valider SIPSim, une implémentation du modèle, sous la forme d'une bibliothèque C++ pour les architectures à mémoire distribuée, nommée SkelGIS, est également proposée dans cette thèse. SkelGIS a été implémentée pour les maillages réguliers à deux dimensions ainsi que pour les simulations sur les réseaux, qui représentent une sous partie des simulations à plusieurs phénomènes physiques. Enfin, cette thèse traite la validation de la bibilothèque SkelGIS, en terme de difficulté de programmation et en terme de performances, par la mise en place de deux cas d'application réels (en collaboration avec des mathématiciens) : une simulation complexe d'écoulement de l'eau sur les surfaces planes, ainsi qu'une simulation d'écoulement du sang dans un réseau artériel. Pour résumer, cette thèse traite du parallélisme implicite pour les simulations numériques basées sur des maillages, du modèle aux cas d'application.


Challenging machine learning classification tasks André Carlos Ponce Leon Ferreira de Carvalho, Universidade de São Paulo at São Carlos, Brazil

One of the main applications of Artificial Intelligence is data classification. Most of the data classification problems reported in the literature deal with only two classes, static classes, classes that have the same level of importance and disjunctive classes. These may be named simple classification problems. In this talk, I will discuss advanced classification problems, like multiclass classification, hierarchical classification, multilabel classification, one-class classification and novelty detection. Research results on some of these issues will be presented. Short Bio: André C. P. L. F. de Carvalho is Full Professor in the department of Computer Science, University of São Paulo, Brasil. His main research interests are data mining, data science and machine learning. Prof. de Carvalho has more than 300 peer reviewed publications, including 10 best papers awards from conferences organized by ACM, IEEE and SBC. He is a member of the International Association for Statistical Computing (IASC) Council and director of the Center of Machine Learning in Data Analysis, University of São Paulo.


A Graph Reduction Machine for Web Service Compositions Martin A. Musicante, Federal University of Rio Grande do Norte, Department of Computer Science, Natal, Brazil

Web Services are the standard for the deployment of Internet applications. Web service composition consists on combining existing web service interfaces to provide new functionality. A number of programming languages have been proposed to describe web service compositions, being BPEL the de-facto standard. Although the formal treatment of web service compositions is recurrent in the literature, the formalization of runtime systems for them is rare. In this work we introduce BP-AM, a graph reduction machine for the implementation of web service composition languages. We define (i) A set of translation functions from a BPEL-like language into graphs and (ii) A set of graph transformation rules in the form of a small-step operational semantics. The execution of a composition (program) consists on transforming its graph by using the rules of the abstract machine. A prototype implementation of BP-AM has been developed in Java. Experiments using this prototype show that service compositions run in BP-AM with performance comparable to that obtained using industrial tools. Joint work with Daniel A. S. Carvalho, Alberto Pardo and Umberto S. Costa.


Vers la construction à large couverture de la représentation du sens de phrases de langue naturelle Benoît Crabbé, Université Paris Diderot-Paris 7, INRIA Rocquencourt

Dans cet exposé, je traiterai le problème d'analyse syntaxique à large couverture de phrases de langues naturelles et de son interface avec la sémantique. Partant de l'hypothèse que la représentation du sens de phrases de langue naturelle s'appuie sur leur structure, je présenterai principalement un algorithme d'analyse syntaxique robuste lexicalisé pour CFG inspiré de GLR et qui propose une désambiguisation des hypothèses d'analyse sur base d'un modèle entièrement discriminant. Une seconde partie de l'exposé, plus succincte, présentera les grandes lignes d'un projet de recherche destiné à augmenter l'algorithme de représentations vectorielles encodant une sémantique distributionnelle.


On the Context-Freeness Problem for Vector Addition Systems Grégoire Sutre, Laboratoire LaBRI - CNRS - Université de Bordeaux

Petri nets, or equivalently vector addition systems (VAS), are widely recognized as a central model for concurrent systems. Many interesting properties are decidable for this class, such as boundedness, reachability, regularity, as well as context-freeness, which is the focus of this work. The context-freeness problem asks whether the trace language of a given VAS is context-free. This problem was shown to be decidable by Schwer in 1992, but the proof is very complex and intricate. In this work, we revisit the context-freeness problem for VAS, and give a simpler proof of decidability. Our approach is based on witnesses of non-context-freeness, that are bounded regular languages satisfying a nesting condition. As a corollary, we obtain that the trace language of a VAS is context-free if, and only if, it has a context-free intersection with every bounded regular language. Our approach allows us to show that the context-freeness problem for VAS, whose complexity was not established so far, is ExpSpace-complete. Joint work with Jérôme Leroux, Vincent Penelle and M. Praveen.


Les capitalistes sociaux : les sentiers de la gloire sur Twitter Nicolas Dugué, LIFO - Université d'Orléans

Les capitalistes sociaux sont des utilisateurs particuliers de Twitter. Ces utilisateurs cherchent à obtenir un maximum de followers par des méthodes que nous décrirons pour gagner de la visibilité sur ce réseau. La visibilité et la potentielle influence obtenues par ces utilisateurs ne sont pas basées sur le contenu de leurs tweets et la crédibilité de leur compte mais sur une accumulation de followers artificielle. Il est donc intéressant de détecter ces utilisateurs et d'étudier leur réel impact sur le média social.


A Linear-Time Algorithm for Computing the Prime Decomposition of a Directed Graph With Regard to the Cartesian Product Christophe Crespelle, LIP - ENS Lyon

We design the first linear-time algorithm for computing the prime decomposition of a digraph G with regard to the cartesian product. A remarkable feature of our solution is that it computes the decomposition of G from the decomposition of its underlying undirected graph, for which there exists a linear-time algorithm. First, this allows our algorithm to remain conceptually very simple and in addition, it provides new insight into the connexions between the directed and undirected versions of the cartesian product of graphs.


Design de structures d'ARN avec contraintes de séquence : une approche à base de langages formels Alain Denise, Université Paris Sud

Le problème du design (ou repliement inverse) de structures secondaires d'ARN est le suivant : la donnée est une structure cible dont on ne connaît pas la séquence. Il s'agit d'engendrer une ou des séquences qui se replieront selon cette structure. Certaines applications en biologie nécessitent d'ajouter des contraintes sur les séquences résultats, par exemple des motifs qui y sont obligatoires ou interdits. Je présenterai une méthode de résolution de ce problème fondée sur l'utilisation de grammaires formelles et d'automates finis, et comment elle a été appliquée dans le cadre d'une collaboration avec une équipe de biologie expérimentale.


Vers l'analyse statique de langages fonctionnels par réécriture et automates d'arbres Thomas Genet, IRISA, Université de Rennes

La complétion d'automates d'arbres est une technique permettant d'approcher l'ensemble des termes accessibles par réécriture. On peut voir la complétion d'automate comme une technique d'ARTMC (Abstract Regular Tree Model Checking) particulière. Si l'on code un programme fonctionnel (pur) par un système de réécriture, la complétion permet d'obtenir un sur-ensemble régulier des résultats de ce programme, i.e. une sur-approximation régulière de l'image de cette fonction. Actuellement, nous étudions l'application de ce principe à l'analyse statique de langages comme OCaml. L'objectif est de proposer un mécanisme de vérification complétant l'inférence de type d'OCaml. En donnant des propriétés régulières sur les valeurs d'entrée de fonctions simples, nous pouvons obtenir des propriétés régulières sur les résultats. Par exemple, il est possible de montrer que l'application d'une fonction filtrant les 0 sur une liste d'entiers quelconques, rend une liste d'entiers différents de de 0. Cependant, pour couvrir un sous-ensemble intéressant d'OCaml, plusieurs défis sont à relever: garantir la terminaison et la précision de l'analyse, prendre en compte les stratégies d'évaluation, prendre en compte l'ordre supérieur, prendre en compte les types built-ins, automatiser la transformation de Ocaml vers les systèmes de réécriture, etc. Concernant ces problèmes, je présenterai l'état des lieux de nos réflexions et travaux ainsi que les questions encore ouvertes.


Mesure de performance des algorithmes de routage pour le HPC Matthieu Perotin, BULL Extreme Computing R&D, Bruyères-Le-Châtel

Les réseaux haute-performance utilisés par les super-calculateurs connaissent en ce moment une évolution rapide, résultant en partie de l'apparition de nouvelles topologies spécifiques. Les algorithmes de routage qui organisent les communications sur ces "fabriques" doivent répondre à un objectif portant à la fois sur les performances applicatives mais aussi sur la résilience. Ce deuxième aspect devient critique avec l'augmentation des tailles des super-calculateurs et la "course à l'exa-flop". La littérature documente de nombreux algorithmes pour chaque type de topologie, voire pour des topologies quelconques, sans pour autant s'attarder sur leur performance effective. Cet exposé tente d'apporter une réponse à cette problématique en la considérant sous un regard: - multi-critère (de multiples fonctions objectif existent) - en-ligne (les pannes surviennent de façon non planifiée) - temps réel (des contraintes fortes existent sur les temps de réaction)


Systèmes multi-agents et culture Loïs Vanhée, Université Montpellier 2 et Universiteit Utrecht

Une des différences clé entre l'humain et l'animal est sa capacité à produire et surtout à échanger et à intégrer une vaste quantité d'information abstraites: une culture. Cette capacité pourtant apparemment simple est cruciale pour construire des phénomènes collectifs bien plus évolués: allant du langage à une structure sociale en passant par la capacité de conserver des acquis techniques. Le lien entre l'individuel et le collectif est particulièrement étudié par les systèmes multi agents, qui servira de technique de référence pour cette présentation. On verra comment l'utiliser pour effectuer des simulations de systèmes sociaux qui utilisent une culture, mais aussi comment s'inspirer de la culture pour améliorer les systèmes multi-agents.


Systèmes complexes : des réseaux génétiques à la ségrégation urbaine Eric Goles, Adolfo Ibáñez University, Santiago, Chili

On presentera des résultats de modélisation de réseaux de régulation génétiques et une famille d'automates à deux dimensions liés au problème de ségrégation de Schelling. Dans le cadre des réseaux d'origine biologique, on discutera de la robustesse du modèle du point de vue dynamique -- c'est-à-dire comment les attracteurs changent avec le mode d'actualisation du réseau. Dans le cadre du problème de ségrégation, on travaillera sur une grille bidimensionnelle où l'on caractérisera les clusters ségrégués selon un paramètre local de tolérance de chaque individu.


Several aspects of probabilistic cellular automata Damien Regnault, IBISC - Université Evry-Val d'Essonne

From the point of view of a computer scientist, deterministic cellular automata are known as a parallel computation model. Different studies have introduced randomness in this model by considering probabilistic transitions. In this talk, I will present the different motivations of these studies as well as the current results and open questions.


Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components Arnaud Lanoix, LINA, Université de Nantes

Dynamic reconfigurations increase the availability and the reliability of component-based systems by allowing their architectures to evolve at runtime. Recently we have proposed a temporal pattern logic, called FTPL, to characterize the correct reconfigurations of component-based systems under some temporal and architectural constraints. As component-based architectures evolve at runtime, there is a need to check these FTPL constraints on the fly, even if only a partial information is expected. Firstly, given a generic component-based model, we review FTPL from a runtime verification point of view. To this end we introduce a new four-valued logic, called RV-FTPL (Runtime Verification for FTPL), characterizing the “potential” (un)satisfiability of the architectural constraints in addition to the basic FTPL semantics. Potential true and potential false values are chosen whenever an observed behaviour has not yet lead to a violation or satisfiability of the property under consideration. Secondly, we present a prototype developed to check at runtime the satisfiability of RV-FTPL formulas when reconfig- uring a Fractal component-based system. The feasability of a runtime property enforcement is also shown. It consists in supervising on the fly the reconfiguration execution against desired RV-FTPL properties. The main contributions are illustrated on the example of a HTTP server architecture.


Une vue d'ensemble de l'extraction Coq Pierre Letouzey, PPS - Université Paris Diderot-Paris 7

Le mécanisme d'extraction de Coq permet de transformer des preuves Coq en programmes fonctionnels. Cet exposé a pour but d'illuster le comportement de cet outil sur plusieurs définitions possibles de la division euclidienne en Coq, ainsi que sur quelques exemples plus avancés. L'extraction est ensuite décrite de manière plus générale: propriétés-clés, principaux cas d'utilisation, forces, faiblesses et perspectives.


First impressions about the use of an embedded low-power manycore processor for HPC Marcio Castro, Universidade Federal do Rio Grande do Sul (Brazil)

The exponential growth in processor performance seems to have reached a turning point. Nowadays, energy efficiency is as important as performance and has become a critical aspect to the development of scalable systems. These strict energy constraints paved the way for the development of manycore processors such as the MPPA-256, which integrates 256 cores in a single low-power chip. In this talk, I will discuss about the use of an embedded low-power manycore processor (MPPA-256) for HPC. In addition to that, I will show some of the performance and energy consumption results obtained when parallelizing a well-known irregular NP-complete problem, the Traveling-Salesman Problem (TSP), on the MPPA-256 as well as on other platforms that comprise general-purpose and low-power multicores. Finally, I will discuss about my current work in cooperation with the BRGM on porting the main kernel of a seismic wave propagation simulator on MPPA-256.


Extraction de code fonctionnel à partir de spécifications inductives Catherine Dubois, ENSIIE

Nous proposons une méthode pour extraire des contenus purement fonctionnels à partir de types inductifs logiques dans le contexte du Calcul des Constructions Inductives (CCI). Cette extraction peut se faire vers des langages fonctionnels à la ML (OCaml, Haskell) ou encore vers le CCI lui-même. Dans ce dernier cas le code fonctionnel extrait s'accompagne de la preuve de sa correction par rapport à la spécification dont il est extrait. Ces travaux (sujet principal de la thèse de Pierre-Nicolas Tollitte) ont donné lieu à un plugin Coq. Cette approche a également été adaptée de manière à synthétiser du code Focalize à partir de propriétés Focalize. La méthode mise en oeuvre s'appuie sur une analyse de consistance de mode qui permet de vérifier qu'un calcul est possible et sur l'utilisation d'une structure de données intermédiaire, le reltree, qui donne de la spécification inductive initiale une vue qui facilite la génération de code. Le processus de génération vers OCaml, Coq et Focalize est en grande partie partagé par les 2 mécanismes de génération de code fonctionnel. Travail réalisé en collaboration avec David Delahaye et Pierre-Nicolas Tollitte.