- Renseignements pratiques
- Enseignement
Contact
LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2
Email:
contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37
Accéder aux Rapports de l'année : 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018
RR-2013-01 Parallel Programming with BSP Homomorphisms
Joeffrey Legaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, Julien Tesson
Résumé : Les squelettes algorithmiques combinés aux homomorphismes de listes jouent un rôle important dans le développement formel d'algorithmiques parallèle. Nous avons conçu une notion d'homomorphisme adapté au parallélisme quasi synchrone (BSP). Dans cet article nous dérivons deux applications en nous basant sur cette théorie: une multiplication matrice creuse par vecteur, et le problème de des plus petites valeurs les plus proches (ANSV). Nous décrivons l'implantation d'un squelette algorithmique dédié dans la bibliothèque OSL et des expériences avec les deux applications.
Mot(s) Clé(s) :
RR-2013-02 Programming and Reasonning with PowerLists in Coq
Frédéric Loulergue, Virginia Niculescu
Résumé : Le développement de programmes parallèles corrects par construction est activité importante puisque, pour les programmes parallèles, la vérification a posteriori est très complexe, et le déboggage extrêmement difficile. Construire des programmes corrects n'est pas une tâche aisée et les méthodologies usuelles pour le faire sont souvent théoriques et non outillées. Une meilleure approche serait de concevoir des outils logiciels basés sur ces théories. Un utilisateur pourrait alors développer des application en implantant des programmes simples satisfaisants certaines conditions facilement, ou idéalement automatiquement, prouvées, à partir desquels un environnement de développement générerait des programmes parallèles efficaces. La théorie des PowerLists et ses variantes est une bonne base théorique pour une telle approche. Par ailleurs l'assistant de preuve Coq est un outil logiciel permettant la modélisation, la preuve, et dans une certaines mesure l'automatisation des preuves, et est à ce titre un bon point de départ pour un tel environnement de développement. Le but de cet article est de modéliser les PowerLists in Coq, d'utiliser cette modélisation pour programmer et raisonner sur des programmes parallèles en Coq. C'est un première étape indispensable à la réalisation d'un environnement pour le développement de programmes parallèles corrects et vérifiables.
Mot(s) Clé(s) :
RR-2013-03 A Constraint Programming Approach for Constrained Clustering
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Résumé : Clustering is an important task in Data Mining and many algorithms have been designed for it. It has been extended to semi-supervised clustering, so as to integrate some previous knowledge on objects that must be or cannot be in the same cluster, and many classical algorithms have been extended to handle such constraints. Other kinds of constraints could be specified by the user, as for instance the sizes of the clusters or their diameters, but adding such constraints generally requires to develop new algorithms. We propose a declarative and generic framework, based on Constraint Programming, which enables to design a clustering task by specifying an optimization criterion and some constraints either on the clusters or on pairs of objects. In our framework, several classical optimization criteria are considered and they can be coupled with different kinds of constraints. Relying on Constraint Programming has two main advantages: the declarativity, which enables to easily add new constraints and the ability to find an optimal solution satisfying all the constraints (when there exists one). On the other hand, computation time depends on the constraints and on their ability to reduce the domain of variables, thus avoiding an exhaustive search.
Mot(s) Clé(s) :
RR-2013-04 Over-approximating Descendants by Synchronized Tree Languages
Yohan Boichut, Jacques Chabin, Pierre Réty
Résumé : Over-approximating the descendants (successors) of a initial set of terms by a rewrite system is used in verification. The success of such verification methods depends on the quality of the approximation. To get better approximations, we are going to use non-regular languages. We present a procedure that always terminates and that computes an over-approximation of descen- dants, using synchronized tree-(tuple) languages expressed by logic programs.
Mot(s) Clé(s) : Rewriting, descendants, tree languages, logic programming
RR-2013-05 Nested Atomic Sections with Thread Escape: A Formal Definition
Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard
Résumé : Nous considérons un langage impératif parallèle simple avec lancement/attente de processus légers et des sections atomiques emboîtées dont les processus légers peuvent s'échapper. Dans ce contexte notre contribution est une définition précise d'atomicité, de bonne synchronisation et une preuve que cette dernière implique la forme forte de la première. Une formalisation de nos résultats dans l'assistant de preuve Coq est disponible.
Mot(s) Clé(s) : sections atomiques, bonne synchronisation, traces de programmes, sémantiques formelles, assistant de preuve
RR-2013-06 Constraint Solving and Language Processing, 7th International Workshop
Denys Duchier, Yannick Parmentier (Eds)
Résumé : These are the proceedings of the seventh International Workshop on Constraint Solving and Language Processing (CSLP). The first CSLP workshop took place in 2004 in Roskilde, Denmark. It opened a decade of research on the role of constraints in the representation and processing of language. While constraints are widely used in many fields, including linguistics, computational linguistics, psycholinguistics, etc., their use and interpretation differs according to the research domain. In this context, the CSLP workshops aim at gathering researchers from various fields to allow them to exchange ideas about their conception of the role of constraints in language understanding and processing.
Mot(s) Clé(s) : Contraintes, Traitement Automatique de la Langue
RR-2013-07 High-level Methodologies for Grammar Engineering, ESSLLI Workshop
Denys Duchier, Yannick Parmentier (Eds)
Résumé : Many grammatical frameworks have been proposed over the last decades to describe the syntax (and semantics) of natural language. Among the most widely used, one may cite (in chronological order) Tree-Adjoining Grammar (TAG) [Joshi et al., 1975], Lexical-Functional Grammar (LFG) [Bresnan and Kaplan, 1982], Combinatory Categorial Grammar (CCG) [Steedman, 1987], or Head- driven Phrase Structure Grammar (HPSG) [Pollard and Sag, 1994]. These frameworks present theoretical and practical interests. From a theoretical point of view, they provide a formal device for the linguist to experiment with her/his theories. From a practical point of view, they make it possible to automatically process natural language in applications such as dialog systems, machine translation, etc. They differ in their expressivity and complexity. Some reveal themselves more adequate for the description of a given language than others. Still, for many of these frameworks, large resources (i.e., grammars) have been designed, at first by hand, and later via dedicated tools (e.g., integrated grammar environments such as XLE for LFG [King et al., 2000]). In this workshop, we are concerned with this complex task of grammar engineering, keeping in mind the two above-mentioned theoretical and practical interests.
Mot(s) Clé(s) : Traitement Automatique de la Langue, Grammaires Formelles
RR-2013-08 Modeling Constrained Clustering Tasks with Bounded Number of Clusters
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Résumé : Constrained clustering is an important task in Data Mining. In the last ten years, many works have been done to extend classical clustering algorithms to handle user-defined constraints, but in general to handle one kind of constraints. In our previous work \cite{DDV-ECML2013}, we have proposed a declarative and generic framework, based on Constraint Programming, which enables to design a clustering task by specifying an optimization criterion and different kinds of user-constraints. The model is designed for a clustering task which divides data in exactly $k$ clusters. In this paper, we present a new model for constrained clustering tasks where the number of clusters is only upper and lower bounded. The new model is simpler and first experiments show that it has a better performance for the diameter based criterion.
Mot(s) Clé(s) :
Les rapports de recherche du LIFO en 2013
RR-2013-01
Parallel Programming with BSP Homomorphisms
Joeffrey Legaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, Julien Tesson
Date : 2013-03-22
Résumé Télécharger
RR-2013-02
Programming and Reasonning with PowerLists in Coq
Frédéric Loulergue, Virginia Niculescu
Date : 2013-03-26
Résumé Télécharger
RR-2013-03
A Constraint Programming Approach for Constrained Clustering
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Date : 2013-05-07
Résumé Télécharger
RR-2013-04
Over-approximating Descendants by Synchronized Tree Languages
Yohan Boichut, Jacques Chabin, Pierre Réty
Date : 2013-04-19
Résumé Télécharger
RR-2013-05
Nested Atomic Sections with Thread Escape: A Formal Definition
Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard
Date : 2013-06-24
Résumé Télécharger
RR-2013-06
Constraint Solving and Language Processing, 7th International Workshop
Denys Duchier, Yannick Parmentier (Eds)
Date : 2013-09-06
Résumé Télécharger
RR-2013-07
High-level Methodologies for Grammar Engineering, ESSLLI Workshop
Denys Duchier, Yannick Parmentier (Eds)
Date : 2013-09-06
Résumé Télécharger
RR-2013-08
Modeling Constrained Clustering Tasks with Bounded Number of Clusters
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Date : 2013-09-11
Résumé Télécharger
Résumés des rapports de recherche
RR-2013-01 Parallel Programming with BSP Homomorphisms
Joeffrey Legaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, Julien Tesson
Résumé : Les squelettes algorithmiques combinés aux homomorphismes de listes jouent un rôle important dans le développement formel d'algorithmiques parallèle. Nous avons conçu une notion d'homomorphisme adapté au parallélisme quasi synchrone (BSP). Dans cet article nous dérivons deux applications en nous basant sur cette théorie: une multiplication matrice creuse par vecteur, et le problème de des plus petites valeurs les plus proches (ANSV). Nous décrivons l'implantation d'un squelette algorithmique dédié dans la bibliothèque OSL et des expériences avec les deux applications.
Mot(s) Clé(s) :
RR-2013-02 Programming and Reasonning with PowerLists in Coq
Frédéric Loulergue, Virginia Niculescu
Résumé : Le développement de programmes parallèles corrects par construction est activité importante puisque, pour les programmes parallèles, la vérification a posteriori est très complexe, et le déboggage extrêmement difficile. Construire des programmes corrects n'est pas une tâche aisée et les méthodologies usuelles pour le faire sont souvent théoriques et non outillées. Une meilleure approche serait de concevoir des outils logiciels basés sur ces théories. Un utilisateur pourrait alors développer des application en implantant des programmes simples satisfaisants certaines conditions facilement, ou idéalement automatiquement, prouvées, à partir desquels un environnement de développement générerait des programmes parallèles efficaces. La théorie des PowerLists et ses variantes est une bonne base théorique pour une telle approche. Par ailleurs l'assistant de preuve Coq est un outil logiciel permettant la modélisation, la preuve, et dans une certaines mesure l'automatisation des preuves, et est à ce titre un bon point de départ pour un tel environnement de développement. Le but de cet article est de modéliser les PowerLists in Coq, d'utiliser cette modélisation pour programmer et raisonner sur des programmes parallèles en Coq. C'est un première étape indispensable à la réalisation d'un environnement pour le développement de programmes parallèles corrects et vérifiables.
Mot(s) Clé(s) :
RR-2013-03 A Constraint Programming Approach for Constrained Clustering
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Résumé : Clustering is an important task in Data Mining and many algorithms have been designed for it. It has been extended to semi-supervised clustering, so as to integrate some previous knowledge on objects that must be or cannot be in the same cluster, and many classical algorithms have been extended to handle such constraints. Other kinds of constraints could be specified by the user, as for instance the sizes of the clusters or their diameters, but adding such constraints generally requires to develop new algorithms. We propose a declarative and generic framework, based on Constraint Programming, which enables to design a clustering task by specifying an optimization criterion and some constraints either on the clusters or on pairs of objects. In our framework, several classical optimization criteria are considered and they can be coupled with different kinds of constraints. Relying on Constraint Programming has two main advantages: the declarativity, which enables to easily add new constraints and the ability to find an optimal solution satisfying all the constraints (when there exists one). On the other hand, computation time depends on the constraints and on their ability to reduce the domain of variables, thus avoiding an exhaustive search.
Mot(s) Clé(s) :
RR-2013-04 Over-approximating Descendants by Synchronized Tree Languages
Yohan Boichut, Jacques Chabin, Pierre Réty
Résumé : Over-approximating the descendants (successors) of a initial set of terms by a rewrite system is used in verification. The success of such verification methods depends on the quality of the approximation. To get better approximations, we are going to use non-regular languages. We present a procedure that always terminates and that computes an over-approximation of descen- dants, using synchronized tree-(tuple) languages expressed by logic programs.
Mot(s) Clé(s) : Rewriting, descendants, tree languages, logic programming
RR-2013-05 Nested Atomic Sections with Thread Escape: A Formal Definition
Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard
Résumé : Nous considérons un langage impératif parallèle simple avec lancement/attente de processus légers et des sections atomiques emboîtées dont les processus légers peuvent s'échapper. Dans ce contexte notre contribution est une définition précise d'atomicité, de bonne synchronisation et une preuve que cette dernière implique la forme forte de la première. Une formalisation de nos résultats dans l'assistant de preuve Coq est disponible.
Mot(s) Clé(s) : sections atomiques, bonne synchronisation, traces de programmes, sémantiques formelles, assistant de preuve
RR-2013-06 Constraint Solving and Language Processing, 7th International Workshop
Denys Duchier, Yannick Parmentier (Eds)
Résumé : These are the proceedings of the seventh International Workshop on Constraint Solving and Language Processing (CSLP). The first CSLP workshop took place in 2004 in Roskilde, Denmark. It opened a decade of research on the role of constraints in the representation and processing of language. While constraints are widely used in many fields, including linguistics, computational linguistics, psycholinguistics, etc., their use and interpretation differs according to the research domain. In this context, the CSLP workshops aim at gathering researchers from various fields to allow them to exchange ideas about their conception of the role of constraints in language understanding and processing.
Mot(s) Clé(s) : Contraintes, Traitement Automatique de la Langue
RR-2013-07 High-level Methodologies for Grammar Engineering, ESSLLI Workshop
Denys Duchier, Yannick Parmentier (Eds)
Résumé : Many grammatical frameworks have been proposed over the last decades to describe the syntax (and semantics) of natural language. Among the most widely used, one may cite (in chronological order) Tree-Adjoining Grammar (TAG) [Joshi et al., 1975], Lexical-Functional Grammar (LFG) [Bresnan and Kaplan, 1982], Combinatory Categorial Grammar (CCG) [Steedman, 1987], or Head- driven Phrase Structure Grammar (HPSG) [Pollard and Sag, 1994]. These frameworks present theoretical and practical interests. From a theoretical point of view, they provide a formal device for the linguist to experiment with her/his theories. From a practical point of view, they make it possible to automatically process natural language in applications such as dialog systems, machine translation, etc. They differ in their expressivity and complexity. Some reveal themselves more adequate for the description of a given language than others. Still, for many of these frameworks, large resources (i.e., grammars) have been designed, at first by hand, and later via dedicated tools (e.g., integrated grammar environments such as XLE for LFG [King et al., 2000]). In this workshop, we are concerned with this complex task of grammar engineering, keeping in mind the two above-mentioned theoretical and practical interests.
Mot(s) Clé(s) : Traitement Automatique de la Langue, Grammaires Formelles
RR-2013-08 Modeling Constrained Clustering Tasks with Bounded Number of Clusters
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Résumé : Constrained clustering is an important task in Data Mining. In the last ten years, many works have been done to extend classical clustering algorithms to handle user-defined constraints, but in general to handle one kind of constraints. In our previous work \cite{DDV-ECML2013}, we have proposed a declarative and generic framework, based on Constraint Programming, which enables to design a clustering task by specifying an optimization criterion and different kinds of user-constraints. The model is designed for a clustering task which divides data in exactly $k$ clusters. In this paper, we present a new model for constrained clustering tasks where the number of clusters is only upper and lower bounded. The new model is simpler and first experiments show that it has a better performance for the diameter based criterion.
Mot(s) Clé(s) :
Université d'Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 