Les outils d’aide à la preuve basés sur la théorie des types permettent à l’utilisateur d’adopter soit un style fonctionnel, soit un style relationnel (c’est-à-dire en utilisant des types inductifs). Chacun des deux styles a des avantages et des inconvénients. Le style relationnel peut être préféré parce qu’il permet à l’utilisateur de décrire seulement ce qui est vrai, de s’abstraire temporairement de la question de la terminaison, et de s’en tenir à une description utilisant des règles. Cependant, une spécification relationnelle n’est pas exécutable.Nous proposons un cadre général pour transformer une spécification inductive en une spécification fonctionnelle, en extrayant à partir de la première une fonction et en produisant éventuellement la preuve de correction de la fonction extraite par rapport à sa spécification inductive. De plus, à partir de modes définis par l’utilisateur, qui permettent de considérer les arguments de la relation comme des entrées ou des sorties (de fonction), nous pouvons extraire plusieurs comportements calculatoires à partir d’un seul type inductif.Nous fournissons également deux implantations de notre approche, l’une dans l’outil d’aide à la preuve Coq et l’autre dans l’environnement Focalize. Les deux sont actuellement distribuées avec leurs outils respectifs. / Proof assistants based on type theory allow the user to adopt either a functional style, or a relational style (e.g., by using inductive types). Both styles have advantages and drawbacks. Relational style may be preferred because it allows the user to describe only what is true, discard momentarily the termination question, and stick to a rule-based description. However, a relational specification is usually not executable.We propose a general framework to turn an inductive specification into a functional one, by extracting a function from the former and eventually produce the proof of soundness of the extracted function w.r.t. its inductive specification. In addition, using user-defined modes which label inputs and outputs, we are able to extract several computational contents from a single inductive type.We also provide two implementations of our approach, one in the Coq proof assistant and the other in the Focalize environnement. Both are currently distributed with the respective tools.

Thèse de doctorat : Chimie et Physico-chimie Moléculaires : Nancy 1 : 2007. / Titre provenant de l'écran-titre. Bibliogr.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal. / Le processus d'acculturation, par lequel les nouveaux arrivants acquièrent les caractéristiques du mode de vie du pays d'accueil, modifie la qualité du régime chez différents groupes ethniques. L'acculturation engendre en effet un déclin de la consommation d'aliments traditionnels parallèlement à l'accroissement de celte de nouveaux aliments, changements élevant souvent les risques de maladies chroniques qui prévalent dans les pays développés. Toutefois, cette relation entre l'acculturation et l'alimentation n'a fait l'objet d'aucune étude chez les Haïtiens. La présente étude a pour but d'évaluer l'acculturation alimentaire et son influence sur rapport nutritionnel et les caractéristiques anthropométriques des Haïtiennes vivant à Montréal. L'acculturation, déterminée par le lieu de naissance et l'âge du sujet à son arrivée au Québec, est représentée dans l'étude par la génération à laquelle appartient le sujet: première ou deuxième génération. La recherche a été réalisée auprès de deux groupes de 25 immigrantes haïtiennes, âgées de 19-49 ans, recrutées majoritairement dans deux églises protestantes haïtiennes. L'acculturation alimentaire a été estimée selon la fréquence d'inclusion d'aliments traditionnels ou nouveaux dans la diète de base pré- et post-immigration pour le premier groupe et post-immigration pour le second. L'apport alimentaire habituel a été déterminé par un questionnaire de fréquence de consommation alimentaire. Des mesures anthropométriques ont aussi été relevées. Les résultats révèlent la conservation de l'usage de certains aliments traditionnels, tels le riz et les légumineuses, chez la majorité des sujets (environ 90%) des deux générations. Néanmoins, la mangue, le maïs moulu, le millet, le manioc et l'igname ont disparu complètement dans le régime de base des sujets de deuxième génération. En revanche, la proportion des sujets consommant régulièrement des céréales à déjeuner, du yogourt et des fromages est passée respectivement de 17%, 36% et 54% des sujets de première génération à 52%, 52% et 72% des sujets de seconde génération. Ces changements alimentaires n'ont modifié ni la répartition des composantes énergétiques du régime ni les apports nutritionnels moyens de la majorité des nutriments étudiés, à l'exception de l'énergie, des protéines, de la vitamine Bg et du sodium qui sont plus élevés chez les sujets de deuxième génération. Ces différences sont dépendantes de l'âge des sujets. Par ailleurs, ces changements se sont traduits par une réduction de moitié des risques d'apports inadéquats en calcium (33% vs 16%) et en vitamine D (12% vs 5%) chez les sujets de seconde génération. Les risques d'apports inadéquats en fer se sont toutefois maintenus chez ce groupe (25% vs 21%). Les sujets de première génération ont un poids, un indice de masse corporelle (IMC), un ratio tour de taille/hanches et une proportion de tissu adipeux supérieurs (p<0,01) à ceux de seconde génération. En effet, une forte proportion (80%) des sujets du premier groupe ont un IMC>=25 comparativement à seulement le quart de ceux du deuxième groupe. Ces différences sont toutefois reliées à l'âge des sujets. Ces résultats montrent donc que l'acculturation alimentaire a un effet bénéfique chez les Haïtiennes de Montréal, quoique le déficit nutritionnel en fer persiste. Il serait donc utile d'orienter les futures études sur la prévalence de l'anémie dans cette communauté.

L'étendue des mouvements que les robots humanoïdes peuvent réaliser est fortement limitée par des contraintes dynamiques. Une loi de commande qui ne prend pas en compte ses res- trictions, d'une manière ou autre, ne va pas réussir d'éviter une chute. La Commande Prédictive est capable de considérer les contraintes sur l'état et le contrôle de manière explicite, ce qui la rend particulièrement appropriée pour le contrôle des mouvements des robots marcheurs.Nous commençons par dévoiler la structure spécifique de ces contraintes, démontrant notamment l'importance des appuis au sol. Nous développons ensuite une condition suffisante pour l'évitement d'une chute et nous proposons une loi de commande prédictive qui y réponde. Cette formulation nous sert ensuite pour la conception des contrôleurs pratiques, capables d'un contrôle plus efficace et plus robuste des robots marcheurs humanoïdes.

L'objectif de ce travail est de fournir des modèles et outils pour simplifier la construction des systèmes distribués à base de composants sécurisés, ainsi que la gestion des propriétés de sécurité, en utilisant des outils de haut niveau d'abstraction pour la configuration et la reconfiguration dynamique. En plus des propriétés d'accessibilité et de communications sécurisées classiques, nous focalisons notre travail sur une propriété des systèmes répartis plus générale : la non-interférence. Cette propriété atteste qu'il ne doit pas y avoir de flux d'information entre des parties publiques et privées du système. Ce qui implique le suivi de l'acheminement de l'information entre les différentes composantes du système distribué. Notre objectif principal est donc de proposer un modèle, accompagné d'un ensemble d'outils, garantissant la propriété de la non-interférence à la construction du système, et ce à une plus grosse granularité : celle des composants. Ces outils permettent de (1) configurer les paramètres de sécurité des composants et des liaisons entre eux, (2) vérifier la propriété de non-interférence dans le code d'un composant et entre les différents composants du système et (3) générer automatiquement le code nécessaire pour appliquer ces propriétés de sécurité. D'autre part, nous proposons une architecture permettant de vérifier dynamiquement la propriété de non-interférence dans un système réparti.

L'étendue des mouvements que les robots humanoïdes peuvent réaliser est fortement limitée par des contraintes dynamiques. Une loi de commande qui ne prend pas en compte ses res- trictions, d'une manière ou autre, ne va pas réussir d'éviter une chute. La Commande Prédictive est capable de considérer les contraintes sur l'état et le contrôle de manière explicite, ce qui la rend particulièrement appropriée pour le contrôle des mouvements des robots marcheurs.Nous commençons par dévoiler la structure spécifique de ces contraintes, démontrant notamment l'importance des appuis au sol. Nous développons ensuite une condition suffisante pour l'évitement d'une chute et nous proposons une loi de commande prédictive qui y réponde. Cette formulation nous sert ensuite pour la conception des contrôleurs pratiques, capables d'un contrôle plus efficace et plus robuste des robots marcheurs humanoïdes. / The range of motions that humanoid robots are able to realize is strongly limited by inherent dynamical constraints so that any control law that does not consider these limitations, in one way or another, will fail to avoid falling. The Model Predictive Control (MPC) technique is capable of handling constraints on the state and the control explicitly, which makes it highly apt for the control of walking robots.We begin by unveiling the specific structure of these constraints, stressing especially the impor- tance of the supports on the ground. We give thereupon a sufficient condition for keeping balance and formulate an MPC law that complies with it. This formulation serves us then for the design of practicable controllers capable of more efficient and more robust control of humanoid robots.

Ce mémoire est composé de trois articles qui s’unissent sous le thème de la recommandation musicale à grande échelle. Nous présentons d’abord une méthode pour effectuer des recommandations musicales en récoltant des étiquettes (tags) décrivant les items et en utilisant cette aura textuelle pour déterminer leur similarité. En plus d’effectuer des recommandations qui sont transparentes et personnalisables, notre méthode, basée sur le contenu, n’est pas victime des problèmes dont souffrent les systèmes de filtrage collaboratif, comme le problème du démarrage à froid (cold start problem). Nous présentons ensuite un algorithme d’apprentissage automatique qui applique des étiquettes à des chansons à partir d’attributs extraits de leur fichier audio. L’ensemble de données que nous utilisons est construit à partir d’une très grande quantité de données sociales provenant du site Last.fm. Nous présentons finalement un algorithme de génération automatique de liste d’écoute personnalisable qui apprend un espace de similarité musical à partir d’attributs audio extraits de chansons jouées dans des listes d’écoute de stations de radio commerciale. En plus d’utiliser cet espace de similarité, notre système prend aussi en compte un nuage d’étiquettes que l’utilisateur est en mesure de manipuler, ce qui lui permet de décrire de manière abstraite la sorte de musique qu’il désire écouter. / This thesis is composed of three papers which unite under the general theme of large-scale music recommendation. The first paper presents a recommendation technique that works by collecting text descriptions of items and using this textual aura to compute the similarity between them using techniques drawn from information retrieval. We show how this representation can be used to explain the similarities between items using terms from the textual aura and further how it can be used to steer the recommender. Because our system is content-based, it is not victim of the usual problems associated with collaborative filtering recommenders like the cold start problem. The second paper presents a machine learning model which automatically applies tags to music. The model uses features extracted from the audio files and was trained on a very large data set constructed with social data from the online community Last.fm. The third paper presents an approach to generating steerable playlists. We first demonstrate a method for learning song transition probabilities from audio features extracted from songs played in professional radio station playlists. We then show that by using this learnt similarity function as a prior, we are able to generate steerable playlists by choosing the next song to play not simply based on that prior, but on a tag cloud that the user is able to manipulate to express the high-level characteristics of the music he wishes to listen to.

Ce mémoire est composé de trois articles qui s’unissent sous le thème de la recommandation musicale à grande échelle. Nous présentons d’abord une méthode pour effectuer des recommandations musicales en récoltant des étiquettes (tags) décrivant les items et en utilisant cette aura textuelle pour déterminer leur similarité. En plus d’effectuer des recommandations qui sont transparentes et personnalisables, notre méthode, basée sur le contenu, n’est pas victime des problèmes dont souffrent les systèmes de filtrage collaboratif, comme le problème du démarrage à froid (cold start problem). Nous présentons ensuite un algorithme d’apprentissage automatique qui applique des étiquettes à des chansons à partir d’attributs extraits de leur fichier audio. L’ensemble de données que nous utilisons est construit à partir d’une très grande quantité de données sociales provenant du site Last.fm. Nous présentons finalement un algorithme de génération automatique de liste d’écoute personnalisable qui apprend un espace de similarité musical à partir d’attributs audio extraits de chansons jouées dans des listes d’écoute de stations de radio commerciale. En plus d’utiliser cet espace de similarité, notre système prend aussi en compte un nuage d’étiquettes que l’utilisateur est en mesure de manipuler, ce qui lui permet de décrire de manière abstraite la sorte de musique qu’il désire écouter. / This thesis is composed of three papers which unite under the general theme of large-scale music recommendation. The first paper presents a recommendation technique that works by collecting text descriptions of items and using this textual aura to compute the similarity between them using techniques drawn from information retrieval. We show how this representation can be used to explain the similarities between items using terms from the textual aura and further how it can be used to steer the recommender. Because our system is content-based, it is not victim of the usual problems associated with collaborative filtering recommenders like the cold start problem. The second paper presents a machine learning model which automatically applies tags to music. The model uses features extracted from the audio files and was trained on a very large data set constructed with social data from the online community Last.fm. The third paper presents an approach to generating steerable playlists. We first demonstrate a method for learning song transition probabilities from audio features extracted from songs played in professional radio station playlists. We then show that by using this learnt similarity function as a prior, we are able to generate steerable playlists by choosing the next song to play not simply based on that prior, but on a tag cloud that the user is able to manipulate to express the high-level characteristics of the music he wishes to listen to.

Aujourd'hui, de plus en plus de systèmes industriels s'appuient sur des applications logicielles temps-réel réparties embarquées (TR2E). La réalisation de ces applications demande de répondre à un ensemble important de contraintes très hétérogènes, voire contradictoires. Pour satisfaire ces contraintes, il est presque toujours nécessaire de fournir à ces systèmes des capacités d'adaptation. Par ailleurs, certaines de ces applications pilotent des systèmes dont la défection peut avoir des conséquences financières - voire humaines - dramatiques. Pour concevoir de telles applications, appelées applications critiques, il faut s'appuyer sur des processus de développpement rigoureux capables de repérer et d'éliminer les erreurs de conception potentielles. Malheureusement, il n'existe pas à notre connaissance de processus de développement capable de traiter ce problème dans le cas où l'adaptation du système à son environnement conduit à modifier sa configuration logicielle. Ce travail de thèse présente une nouvelle méthodologie qui répond à cette problématique en s'appuyant sur la notion de mode de fonctionnement : chacun des comportements possibles du système est représenté par le biais d'un mode de fonctionnement auquel est associé une configuration logicielle. La spécification des règles de transition entre ces modes de fonctionnement permet alors de générer l'implantation des mécanismes de changement de mode, ainsi que des reconfigurations logicielles associées. Le code ainsi produit respecte les contraintes de réalisation des systèmes critiques et implante des mécanismes de reconfiguration sûrs et analysables. Pour ce faire, nous avons défini un nouveau langage de description d'architecture (COAL : Component Oriented Architecture Language) qui permet de bénéficier à la fois des avantages du génie logiciel à base de composants (de type Lightweight CCM), et des techniques d'analyse, de déploiement et de configuration statique, qu'apporte l'utilisation des langages de description d'architecture (et en particulier AADL : Architecture Analysis and Description Language). Nous avons alors réalisé un nouveau framework à composant, MyCCM-HI (Make your Component Container Model - High Integrity), qui exploite les constructions de COAL pour (i) générer le modèle AADL permettant de réaliser le déploiement et la configuration statique de l'application TR2E, (ii) générer le code de déploiement et de configuration des composants logiciels de type Lightweight CCM, (iii) générer le code correspondant aux mécanismes d'adaptation du système, et (iv) analyser formellement le comportement du système, y compris en cours d'adaptation. Ce framework à composant est disponible au téléchargement à l'adresse http ://myccm-hi.sourceforge.net.