- Contacts/Reaching LIFO
- Teaching
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
Go to Research Reports of Year : 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
Abstract : Algorithmic skeletons in conjunction with list homomorphisms play an important role in formal development of parallel algorithms. We have designed a notion of homomorphism dedicated to bulk synchronous parallelism. In this paper we derive two application using this theory: sparse matrix vector multiplication and the all nearest smaller values problem. We implement a support for BSP homomorphism in the Orléans Skeleton Library and experiment it with these two applications.
Keywords :
RR-2013-02 Programming and Reasonning with PowerLists in Coq
Frédéric Loulergue, Virginia Niculescu
Abstract : For parallel programs correctness by construction is an essential feature since debugging is almost impossible. To build correct programs by constructions is not a simple task, and usually the methodologies used for this purpose are rather theoretical based on a pen-and-paper style. A better approach could be based on tools and theories that allow a user to develop an efficient parallel application by implementing easily simple programs satisfying conditions, ideally automatically, proved. PowerLists theory and its variants represent a good theoretical base for an approach like this, and Coq proof assistant is a tool that could be used for automatic proofs. The goal of this paper is to model the PowerList theory in Coq, and to use this modelling to program and reason on parallel programs in Coq. This represents the first step in building a framework that ease the development of correct and verifiable parallel programs.
Keywords :
RR-2013-03 A Constraint Programming Approach for Constrained Clustering
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Abstract : 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.
Keywords :
RR-2013-04 Over-approximating Descendants by Synchronized Tree Languages
Yohan Boichut, Jacques Chabin, Pierre Réty
Abstract : 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.
Keywords : 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
Abstract : We consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. A formalisation of our results in the Coq proof assistant is also available.
Keywords : atomic sections, well-synchronisation, program traces, formal semantics, proof assistant
RR-2013-06 Constraint Solving and Language Processing, 7th International Workshop
Denys Duchier, Yannick Parmentier (Eds)
Abstract : 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.
Keywords : Contraintes, Traitement Automatique de la Langue
RR-2013-07 High-level Methodologies for Grammar Engineering, ESSLLI Workshop
Denys Duchier, Yannick Parmentier (Eds)
Abstract : 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.
Keywords : 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
Abstract : 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.
Keywords :
LIFO Research Report for Year 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
Abstract Download
RR-2013-02
Programming and Reasonning with PowerLists in Coq
Frédéric Loulergue, Virginia Niculescu
Date : 2013-03-26
Abstract Download
RR-2013-03
A Constraint Programming Approach for Constrained Clustering
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Date : 2013-05-07
Abstract Download
RR-2013-04
Over-approximating Descendants by Synchronized Tree Languages
Yohan Boichut, Jacques Chabin, Pierre Réty
Date : 2013-04-19
Abstract Download
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
Abstract Download
RR-2013-06
Constraint Solving and Language Processing, 7th International Workshop
Denys Duchier, Yannick Parmentier (Eds)
Date : 2013-09-06
Abstract Download
RR-2013-07
High-level Methodologies for Grammar Engineering, ESSLLI Workshop
Denys Duchier, Yannick Parmentier (Eds)
Date : 2013-09-06
Abstract Download
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
Abstract Download
Abstracts of Research Reports
RR-2013-01 Parallel Programming with BSP Homomorphisms
Joeffrey Legaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, Julien Tesson
Abstract : Algorithmic skeletons in conjunction with list homomorphisms play an important role in formal development of parallel algorithms. We have designed a notion of homomorphism dedicated to bulk synchronous parallelism. In this paper we derive two application using this theory: sparse matrix vector multiplication and the all nearest smaller values problem. We implement a support for BSP homomorphism in the Orléans Skeleton Library and experiment it with these two applications.
Keywords :
RR-2013-02 Programming and Reasonning with PowerLists in Coq
Frédéric Loulergue, Virginia Niculescu
Abstract : For parallel programs correctness by construction is an essential feature since debugging is almost impossible. To build correct programs by constructions is not a simple task, and usually the methodologies used for this purpose are rather theoretical based on a pen-and-paper style. A better approach could be based on tools and theories that allow a user to develop an efficient parallel application by implementing easily simple programs satisfying conditions, ideally automatically, proved. PowerLists theory and its variants represent a good theoretical base for an approach like this, and Coq proof assistant is a tool that could be used for automatic proofs. The goal of this paper is to model the PowerList theory in Coq, and to use this modelling to program and reason on parallel programs in Coq. This represents the first step in building a framework that ease the development of correct and verifiable parallel programs.
Keywords :
RR-2013-03 A Constraint Programming Approach for Constrained Clustering
Thi-Bich-Hanh Dao, Khanh-Chuong Duong, Christel Vrain
Abstract : 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.
Keywords :
RR-2013-04 Over-approximating Descendants by Synchronized Tree Languages
Yohan Boichut, Jacques Chabin, Pierre Réty
Abstract : 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.
Keywords : 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
Abstract : We consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. A formalisation of our results in the Coq proof assistant is also available.
Keywords : atomic sections, well-synchronisation, program traces, formal semantics, proof assistant
RR-2013-06 Constraint Solving and Language Processing, 7th International Workshop
Denys Duchier, Yannick Parmentier (Eds)
Abstract : 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.
Keywords : Contraintes, Traitement Automatique de la Langue
RR-2013-07 High-level Methodologies for Grammar Engineering, ESSLLI Workshop
Denys Duchier, Yannick Parmentier (Eds)
Abstract : 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.
Keywords : 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
Abstract : 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.
Keywords :
University of Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 