A Type-Preserving Compiler from System F to Typed Assembly Language

L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type.

Modularité massive ou construction sociale? : une analyse de l'approche psychoévolutionniste de Cosmides et Tooby.

Ce mémoire se veut un examen épistémologique de la thèse psychoévolutionniste de Leda Cosmides et John Tooby, principalement en ce qui concerne la modularité massive. Nous avons tâché de voir si la modularité massive permet de rendre compte des processus mentaux complexes en nous penchant plus particulièrement sur le cas des émotions. Nous explorons d'abord la thèse de Cosmides et Tooby en la distinguant d'avec d'autres conceptions comme l'écologie béhaviorale et en expliquant le rôle particulier que jouent les émotions au sein de la théorie. Nous analysons ensuite la thèse de la modularité massive et les différents arguments théoriques ou empiriques qui l'appuient, et évaluons finalement des critiques de la modularité émises par certains philosophes, dont David Buller.

Sur l’utilisation du langage de programmation Scheme pour le développement de jeux vidéo

Ce mémoire vise à recenser les avantages et les inconvénients de l'utilisation du langage de programmation fonctionnel dynamique Scheme pour le développement de jeux vidéo. Pour ce faire, la méthode utilisée est d'abord basée sur une approche plus théorique. En effet, une étude des besoins au niveau de la programmation exprimés par ce type de développement, ainsi qu'une description détaillant les fonctionnalités du langage Scheme pertinentes au développement de jeux vidéo sont données afin de bien mettre en contexte le sujet. Par la suite, une approche pratique est utilisée en effectuant le développement de deux jeux vidéo de complexités croissantes: Space Invaders et Lode Runner. Le développement de ces jeux vidéo a mené à l'extension du langage Scheme par plusieurs langages spécifiques au domaine et bibliothèques, dont notamment un système de programmation orienté objets et un système de coroutines. L'expérience acquise par le développement de ces jeux est finalement comparée à celle d'autres développeurs de jeux vidéo de l'industrie qui ont utilisé Scheme pour la création de titres commerciaux. En résumé, l'utilisation de ce langage a permis d'atteindre un haut niveau d'abstraction favorisant la modularité des jeux développés sans affecter les performances de ces derniers.

Le langage humain est-il une adaptation biologique? : un regard critique sur une explication adaptationniste

Pinker et Bloom (1990), deux représentants de la psychologie évolutionniste, soutiennent que le langage est une adaptation biologique ayant pour fonction la communication. Ils prétendent ainsi jeter un éclairage sur l’origine et l’évolution du langage. Le présent mémoire propose une analyse critique de leur argumentation, et ce, du point de vue de la philosophie de la biologie. D’une part, il tente de dissiper la confusion entourant la conception du langage adoptée par Pinker et Bloom, afin de mieux définir le trait censé constituer une adaptation biologique. Ce faisant, ce mémoire fait ressortir certains présupposés de leur conception du langage et en souligne l’aspect problématique. En ce sens, les concepts d’innéité, de modularité, de grammaire universelle et de systématicité sont abordés de façon critique. D’autre part, ce travail entend expliciter un concept clé de l’argumentation de Pinker et Bloom : celui d’adaptation. L’analyse montre que l’opposition entre adaptationnisme et anti-adaptationnisme tient, dans le cas présent, à une divergence quant à la façon de définir l’adaptation biologique. Une distinction importante doit être faite entre une adaptation résultant exclusivement de la sélection naturelle dans un contexte fonctionnel particulier et une adaptation qui n’exclut pas a priori d’autres facteurs évolutifs, dont l’exaptation. Dans la mesure où l’argumentation de Pinker et Bloom conduit à affirmer que le langage constitue une adaptation seulement au deuxième sens du terme, ce mémoire montre qu’ils ne sont pas à même de rendre compte de l’origine du langage.

A Categorical Framework for the Specification and the Verification of Aspect Oriented Systems

Un objectif principal du génie logiciel est de pouvoir produire des logiciels complexes, de grande taille et fiables en un temps raisonnable. La technologie orientée objet (OO) a fourni de bons concepts et des techniques de modélisation et de programmation qui ont permis de développer des applications complexes tant dans le monde académique que dans le monde industriel. Cette expérience a cependant permis de découvrir les faiblesses du paradigme objet (par exemples, la dispersion de code et le problème de traçabilité). La programmation orientée aspect (OA) apporte une solution simple aux limitations de la programmation OO, telle que le problème des préoccupations transversales. Ces préoccupations transversales se traduisent par la dispersion du même code dans plusieurs modules du système ou l’emmêlement de plusieurs morceaux de code dans un même module. Cette nouvelle méthode de programmer permet d’implémenter chaque problématique indépendamment des autres, puis de les assembler selon des règles bien définies. La programmation OA promet donc une meilleure productivité, une meilleure réutilisation du code et une meilleure adaptation du code aux changements. Très vite, cette nouvelle façon de faire s’est vue s’étendre sur tout le processus de développement de logiciel en ayant pour but de préserver la modularité et la traçabilité, qui sont deux propriétés importantes des logiciels de bonne qualité. Cependant, la technologie OA présente de nombreux défis. Le raisonnement, la spécification, et la vérification des programmes OA présentent des difficultés d’autant plus que ces programmes évoluent dans le temps. Par conséquent, le raisonnement modulaire de ces programmes est requis sinon ils nécessiteraient d’être réexaminés au complet chaque fois qu’un composant est changé ou ajouté. Il est cependant bien connu dans la littérature que le raisonnement modulaire sur les programmes OA est difficile vu que les aspects appliqués changent souvent le comportement de leurs composantes de base [47]. Ces mêmes difficultés sont présentes au niveau des phases de spécification et de vérification du processus de développement des logiciels. Au meilleur de nos connaissances, la spécification modulaire et la vérification modulaire sont faiblement couvertes et constituent un champ de recherche très intéressant. De même, les interactions entre aspects est un sérieux problème dans la communauté des aspects. Pour faire face à ces problèmes, nous avons choisi d’utiliser la théorie des catégories et les techniques des spécifications algébriques. Pour apporter une solution aux problèmes ci-dessus cités, nous avons utilisé les travaux de Wiels [110] et d’autres contributions telles que celles décrites dans le livre [25]. Nous supposons que le système en développement est déjà décomposé en aspects et classes. La première contribution de notre thèse est l’extension des techniques des spécifications algébriques à la notion d’aspect. Deuxièmement, nous avons défini une logique, LA , qui est utilisée dans le corps des spécifications pour décrire le comportement de ces composantes. La troisième contribution consiste en la définition de l’opérateur de tissage qui correspond à la relation d’interconnexion entre les modules d’aspect et les modules de classe. La quatrième contribution concerne le développement d’un mécanisme de prévention qui permet de prévenir les interactions indésirables dans les systèmes orientés aspect.

Les neurosciences cognitives du langage, de l'autisme et des styles cognitifs

VERSION ANGLAISE DISPONIBLE AU DÉPARTEMENT; THÈSE RÉALISÉE CONJOINTEMENT AVEC L'ÉCOLE DES SCIENCES DE LA COMMUNICATION DE L'UNIVERSITÉ MCGILL (DRS. K. STEINHAUER ET J.E. DRURY).

Relargage d’ions métalliques après l’arthroplastie de la hanche à grand diamètre avec couple de frottement métal sur métal

La dégénérescence articulaire sévère de la hanche est une pathologie fréquente et son traitement ultime est le remplacement prothétique. L’arthroplastie la plus répandue au monde est la prothèse totale de hanche (PTH) avec un couple de frottement métal-sur-polyéthylène (MPE). Cependant ce type d’intervention présente une longévité limitée à cause de l’usure de PE et ne convient pas aux patients actifs souffrant de coxarthrose sévère tôt dans leur vie. Afin de palier à ce problème, une nouvelle génération de surfaces de frottement métal-sur-métal (MM) est actuellement employée. Ces surfaces de frottement sont utilisées en PTH avec tête de 28 mm, en resurfaçage (RH) et avec la PTH à tête de grand diamètre. Alors qu’il y a beaucoup d’évidence à l’égard du bon fonctionnement des implants PTH 28 mm et du RH, les données quant aux performances in vivo des PTH MM à grand diamètre manquent. Malgré cela, ces implants sont utilisés à grande échelle. Dans un premier temps, l’objectif de ce travail de recherche était d’évaluer l’effet et de comparer les taux d’ions chrome (Cr) et cobalt (Co) chez des sujets porteurs de PTH MM à grand diamètre à ceux de 64 porteurs de RH, tous deux possédant des surfaces de frottement aux propriétés tribologiques identiques. Dans un deuxième temps, nous avons comparé les taux ioniques (Cr, Co et titane (Ti)) entre quatre PTH MM à grand diamètre provenant de fabricants différents (Zimmer, DePuy, Smith & Nephew et Biomet). Les mesures d’ions étaient effectuées dans le sang entier dans un laboratoire indépendant par la technique de spectrophotométrie de masse à haute résolution HR-ICP-MS, pour l’ensemble de ce travail de recherche. Les deux comparaisons ont démontré le rôle crucial joué par la modularité au niveau de la jonction tête-col des PTH MM à grand diamètre. En effet, des écarts considérables dans les concentrations ioniques de Co ont été retrouvés entre les RH et PTH Durom ayant un couple de frottement identique, ainsi qu’entre les 4 différents designs de PTH MM à grand diamètre comparés entre eux. La PTH MM à grand diamètre Durom était la moins favorable alors que celle de Biomet était la plus performante. Nos observations démontrent que des sources inattendues comme la jonction tête-col de certains implants PTH MM à grand diamètre peuvent contribuer au relargage ionique systémique. Une meilleure compréhension de ce phénomène est indispensable avant l’utilisation clinque de nouveaux implants de ce type.

Cogestion des ressources naturelles : une approche structurale pour quantifier la contribution des réseaux d'acteurs à la résilience des systèmes socio-écologiques

Alors que les activités anthropiques font basculer de nombreux écosystèmes vers des régimes fonctionnels différents, la résilience des systèmes socio-écologiques devient un problème pressant. Des acteurs locaux, impliqués dans une grande diversité de groupes — allant d’initiatives locales et indépendantes à de grandes institutions formelles — peuvent agir sur ces questions en collaborant au développement, à la promotion ou à l’implantation de pratiques plus en accord avec ce que l’environnement peut fournir. De ces collaborations répétées émergent des réseaux complexes, et il a été montré que la topologie de ces réseaux peut améliorer la résilience des systèmes socio-écologiques (SSÉ) auxquels ils participent. La topologie des réseaux d’acteurs favorisant la résilience de leur SSÉ est caractérisée par une combinaison de plusieurs facteurs : la structure doit être modulaire afin d’aider les différents groupes à développer et proposer des solutions à la fois plus innovantes (en réduisant l’homogénéisation du réseau), et plus proches de leurs intérêts propres ; elle doit être bien connectée et facilement synchronisable afin de faciliter les consensus, d’augmenter le capital social, ainsi que la capacité d’apprentissage ; enfin, elle doit être robuste, afin d’éviter que les deux premières caractéristiques ne souffrent du retrait volontaire ou de la mise à l’écart de certains acteurs. Ces caractéristiques, qui sont relativement intuitives à la fois conceptuellement et dans leur application mathématique, sont souvent employées séparément pour analyser les qualités structurales de réseaux d’acteurs empiriques. Cependant, certaines sont, par nature, incompatibles entre elles. Par exemple, le degré de modularité d’un réseau ne peut pas augmenter au même rythme que sa connectivité, et cette dernière ne peut pas être améliorée tout en améliorant sa robustesse. Cet obstacle rend difficile la création d’une mesure globale, car le niveau auquel le réseau des acteurs contribue à améliorer la résilience du SSÉ ne peut pas être la simple addition des caractéristiques citées, mais plutôt le résultat d’un compromis subtil entre celles-ci. Le travail présenté ici a pour objectifs (1), d’explorer les compromis entre ces caractéristiques ; (2) de proposer une mesure du degré auquel un réseau empirique d’acteurs contribue à la résilience de son SSÉ ; et (3) d’analyser un réseau empirique à la lumière, entre autres, de ces qualités structurales. Cette thèse s’articule autour d’une introduction et de quatre chapitres numérotés de 2 à 5. Le chapitre 2 est une revue de la littérature sur la résilience des SSÉ. Il identifie une série de caractéristiques structurales (ainsi que les mesures de réseaux qui leur correspondent) liées à l’amélioration de la résilience dans les SSÉ. Le chapitre 3 est une étude de cas sur la péninsule d’Eyre, une région rurale d’Australie-Méridionale où l’occupation du sol, ainsi que les changements climatiques, contribuent à l’érosion de la biodiversité. Pour cette étude de cas, des travaux de terrain ont été effectués en 2010 et 2011 durant lesquels une série d’entrevues a permis de créer une liste des acteurs de la cogestion de la biodiversité sur la péninsule. Les données collectées ont été utilisées pour le développement d’un questionnaire en ligne permettant de documenter les interactions entre ces acteurs. Ces deux étapes ont permis la reconstitution d’un réseau pondéré et dirigé de 129 acteurs individuels et 1180 relations. Le chapitre 4 décrit une méthodologie pour mesurer le degré auquel un réseau d’acteurs participe à la résilience du SSÉ dans lequel il est inclus. La méthode s’articule en deux étapes : premièrement, un algorithme d’optimisation (recuit simulé) est utilisé pour fabriquer un archétype semi-aléatoire correspondant à un compromis entre des niveaux élevés de modularité, de connectivité et de robustesse. Deuxièmement, un réseau empirique (comme celui de la péninsule d’Eyre) est comparé au réseau archétypique par le biais d’une mesure de distance structurelle. Plus la distance est courte, et plus le réseau empirique est proche de sa configuration optimale. La cinquième et dernier chapitre est une amélioration de l’algorithme de recuit simulé utilisé dans le chapitre 4. Comme il est d’usage pour ce genre d’algorithmes, le recuit simulé utilisé projetait les dimensions du problème multiobjectif dans une seule dimension (sous la forme d’une moyenne pondérée). Si cette technique donne de très bons résultats ponctuellement, elle n’autorise la production que d’une seule solution parmi la multitude de compromis possibles entre les différents objectifs. Afin de mieux explorer ces compromis, nous proposons un algorithme de recuit simulé multiobjectifs qui, plutôt que d’optimiser une seule solution, optimise une surface multidimensionnelle de solutions. Cette étude, qui se concentre sur la partie sociale des systèmes socio-écologiques, améliore notre compréhension des structures actorielles qui contribuent à la résilience des SSÉ. Elle montre que si certaines caractéristiques profitables à la résilience sont incompatibles (modularité et connectivité, ou — dans une moindre mesure — connectivité et robustesse), d’autres sont plus facilement conciliables (connectivité et synchronisabilité, ou — dans une moindre mesure — modularité et robustesse). Elle fournit également une méthode intuitive pour mesurer quantitativement des réseaux d’acteurs empiriques, et ouvre ainsi la voie vers, par exemple, des comparaisons d’études de cas, ou des suivis — dans le temps — de réseaux d’acteurs. De plus, cette thèse inclut une étude de cas qui fait la lumière sur l’importance de certains groupes institutionnels pour la coordination des collaborations et des échanges de connaissances entre des acteurs aux intérêts potentiellement divergents.

La notion de l’explosion de la coopération et ses implications chez Kim Sterelny.

Le concept de coopération est souvent utilisé dans le domaine de l’éthique et de la politique pour illustrer et comprendre l’alignement des comportements associatifs entre les êtres humains. En lien avec ce concept, notre recherche portera sur la première question de savoir si Kim Sterelny (2003) réussit à produire un modèle théorique permettant d’expliquer les origines et les mécanismes de la coopération humaine. Notre recherche portera aussi sur la deuxième question de savoir s’il arrive à se servir de ce modèle pour infirmer la thèse de la modularité massive. Ainsi, ce mémoire traitera successivement du problème de la coopération, de la théorie de la sélection de groupe, du déclencheur écologique de la coopération des hominidés, des notions de coalition, d’exécution et d’engagement et finalement de la thèse de la modularité massive. Par l’examen de ces sujets, nous souhaitons démontrer que Sterelny n’arrive qu’à fournir une esquisse probable des origines et du développement de la coopération humaine et que sa critique de la thèse de la modularité massive n’arrive pas à infirmer cette dernière.